******************************************** 
* KeY Byte Code Installation               * 
* Version 0.9                              *
********************************************


(1) Requirements: 
-------------------------------------

Operating Systems: Linux/Unix 
                   Windows NT, 2000 or XP

Java 2 SDK, Version 1.3.x or 1.4.x (already installed)

Together Control Center, Version 6.0 or 6.0.1 (already installed)

(Remark: Although KeY supports Java2 SDK 1.4, you may have slight
problems running Together 6.0.1 with this Java version.)

Needed additional Libraries:
	antlr.jar Version >= 2.7.1: parser generator
	dresden-ocl-demo.jar: ocl parser
	xerces.jar version 1.4.4: used by tudresden.jar
	recoder.jar version 0.70KeY: a transformation framework for java
			             patched by KeY

Optionally, KeY can make use of the following binaries:
	ESC Java's decision procedure `Simplify´
	Grammatical Framework

(2) Contents of the KeY-Distribution
-------------------------------------

  At the KeY-Homepage you can find the following parts:

   * README_vxx.install: this file
   * KeY_vxx.tgz: the KeY-system in the jar-file version. That is the
         distribution version without the source code.
   * KeYExtLib_vxx.tgz: contains the external libraries (see above) 
   * quicktour_vxx.ps.gz: a short tutorial
   * KeYDemo_vxx.tgz: example for KeY used in the tutorial


(3) Installation (Byte Code)
-------------------------------------
	1) Copy the KeY_vxxx.tgz to a temporary directory; 
	   Here: tmp/

	2) Unpack KeY_vxxx.tgz 

		Linux: 
		   tar -xzvf KeY_vxxx.tgz 

		Windows ( use your favorite unpack program that can handle
			  tar-gzipped archives , e.g. WinZip) 

	3) The following files should be found in the directory (tmp/):
		setup.jar  key.jar LICENSE.TXT

	4) Change to tmp/ and start installation wizard:
               java -jar setup.jar 
           ( or (depends on platform): double-click on setup.jar )

	5) Follow the instructions of the wizard.

	   
	6) (This step is only necessary if you want to make use of the
	    authoring tool Grammatical Framework and/or the decision
	    procedure Simplify.)

           If you download Simplify not from the KeY-website but
           elsewhere e.g. directly from Compaq (as part of ESC/Java)
           follow the intallation instructions given there. Then
           rename the Simplify binary which could be named something like
           Simplify Simplify-1.5.4.linux (Linux version) or 
           Simplify-1.5.4.exe (Windows) to just 'Simplify' resp. 
           'Simplify.exe'. When using Linux make sure that the file is
           is executable (you can make a file executable by issuing the
           command 'chmod a+x filename').

	   Make sure that the path where the binaries `Simplify´ and
	   `gf´ (Grammatical Framework) reside is included in your PATH
	   environment variable. If not, use (e.g., in the csh to
	   include Simplify which is assumed to be located in
	   ~/simplify):

		setenv PATH ~/simplify:$PATH

           In bash-syntax the above command is
       
                export PATH=$PATH:~/simplify
	   


(4) Start KeY 
-------------------------------

	Change to the chosen installation directory 

	Go to subdirectory bin and run 'startkey' (Windows: 'startkey.bat')

	If you want to start the standalone prover without Together,
	run 'startProver' (Windows: 'startProver.bat') instead.

	
If you encounter problems please send a message to

		key@mail.informatik.kit.edu