(*.evaluate isac (all the code of the kernel) and isactest

    (c) Walther Neuper 1997

   /usr/local/Isabelle2002/bin/isabelle HOL-Real-Isac

   /usr/local/Isabelle2002/bin/isabelle HOL-Real

   cd"~/proto2/isac/src/sml"; use"RCODE-root.sml";

   use"ROOT.ML";

   use"RTEST-root.sml";

 .*)

 (*.please change HERE and in ROOT.ML accordingly, 

    if you store a new heap ...*)

 val version_isac = "WN0710-calcResponse";

 print_depth 1;(*reduces verbosity of stdout*)

 (*.this function from Isabelle2002/src/Pure/library.ML is overwritten

   by some Isabelle2002 theory file; thus reestablished for isac.*)

 fun find_first _ [] = None

   | find_first pred (x :: xs) =

     if pred x then Some x else find_first pred xs;

 fun swap (x, y) = (y, x);

 (*HACK.WN080107*) val sstr = str;

 "**** build the isac kernel = math-engine + IsacKnowledge ";

 "**** build the math-engine ******************************";

 use"library.sml";

 use"calcelems.sml";

 cd "Scripts";

  	use"term_G.sml";

  	use"calculate.sml";

  	use"rewrite.sml";

  	use_thy"Script";

 (*      remove_thy"ListG";

  	use_thy"~/proto2/isac/src/sml/Scripts/Script";

  	*)

  	use"scrtools.sml";

  	cd ".."; 

 cd "ME";

  	use"mstools.sml";

  	use"ctree.sml";

  	use"ptyps.sml"; 

  	use"generate.sml";

  	use"calchead.sml";

  	use"appl.sml";

  	use"rewtools.sml";

  	use"script.sml";

  	use"solve.sml";

 	use"inform.sml"; 

  	use"mathengine.sml";

  	cd ".."; 

 cd "xmlsrc";

  	use"mathml.sml";

  	use"datatypes.sml";        

  	use"pbl-met-hierarchy.sml";      

  	use"thy-hierarchy.sml";    

  	use"interface-xml.sml";

  	cd "..";

 cd"FE-interface";

  	use"messages.sml";

 	use"states.sml";

 	use"interface.sml";

  	cd "..";

 use"print_exn_G.sml";

 "**** build math-engine complete *************************";

 "**** build the IsacKnowledge ****************************";

  cd "IsacKnowledge";

  	use_thy"Isac"; (*evaluates ALL thys depending on the root 'Isac'*)

  (*     remove_thy"Typefix";

  	use_thy"~/proto2/isac/src/sml/IsacKnowledge/Isac";

         *)

  	cd "..";

 "**** build IsacKnowledge complete ***********************";

 "**** build isac kernel complete *************************";

 states:=[];

 print_depth 3;