1.1 --- a/src/Tools/isac/RCODE-root.sml	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,81 +0,0 @@
     1.4 -(*.evaluate isac (all the code of the kernel) and isactest
     1.5 -   (c) Walther Neuper 1997
     1.6 -
     1.7 -  /usr/local/Isabelle2002/bin/isabelle HOL-Real-Isac
     1.8 -
     1.9 -  /usr/local/Isabelle2002/bin/isabelle HOL-Real
    1.10 -  cd"~/proto2/isac/src/sml"; use"RCODE-root.sml";
    1.11 -
    1.12 -  use"ROOT.ML";
    1.13 -  use"RTEST-root.sml";
    1.14 -.*)
    1.15 -
    1.16 -(*.please change HERE and in ROOT.ML accordingly, 
    1.17 -   if you store a new heap ...*)
    1.18 -val version_isac = "WN0710-calcResponse";
    1.19 -
    1.20 -print_depth 1;(*reduces verbosity of stdout*)
    1.21 -
    1.22 -(*.this function from Isabelle2002/src/Pure/library.ML is overwritten
    1.23 -  by some Isabelle2002 theory file; thus reestablished for isac.*)
    1.24 -fun find_first _ [] = NONE
    1.25 -  | find_first pred (x :: xs) =
    1.26 -    if pred x then SOME x else find_first pred xs;
    1.27 -fun swap (x, y) = (y, x);
    1.28 -(*HACK.WN080107*) val sstr = str;
    1.29 -
    1.30 -"**** build the isac kernel = math-engine + IsacKnowledge ";
    1.31 -"**** build the math-engine ******************************";
    1.32 -use"library.sml";
    1.33 -use"calcelems.sml";
    1.34 -cd "Scripts";
    1.35 - 	use"term_G.sml";
    1.36 - 	use"calculate.sml";
    1.37 - 	use"rewrite.sml";
    1.38 - 	use_thy"Script";
    1.39 -(*      remove_thy"ListG";
    1.40 - 	use_thy"~/proto2/isac/src/sml/Scripts/Script";
    1.41 - 	*)
    1.42 - 	use"scrtools.sml";
    1.43 - 	cd ".."; 
    1.44 -cd "ME";
    1.45 - 	use"mstools.sml";
    1.46 - 	use"ctree.sml";
    1.47 - 	use"ptyps.sml"; 
    1.48 - 	use"generate.sml";
    1.49 - 	use"calchead.sml";
    1.50 - 	use"appl.sml";
    1.51 - 	use"rewtools.sml";
    1.52 - 	use"script.sml";
    1.53 - 	use"solve.sml";
    1.54 -	use"inform.sml"; 
    1.55 - 	use"mathengine.sml";
    1.56 - 	cd ".."; 
    1.57 -cd "xmlsrc";
    1.58 - 	use"mathml.sml";
    1.59 - 	use"datatypes.sml";        
    1.60 - 	use"pbl-met-hierarchy.sml";      
    1.61 - 	use"thy-hierarchy.sml";    
    1.62 - 	use"interface-xml.sml";
    1.63 - 	cd "..";
    1.64 -cd"FE-interface";
    1.65 - 	use"messages.sml";
    1.66 -	use"states.sml";
    1.67 -	use"interface.sml";
    1.68 - 	cd "..";
    1.69 -use"print_exn_G.sml";
    1.70 -"**** build math-engine complete *************************";
    1.71 - 
    1.72 -"**** build the IsacKnowledge ****************************";
    1.73 - cd "IsacKnowledge";
    1.74 - 	use_thy"Isac"; (*evaluates ALL thys depending on the root 'Isac'*)
    1.75 -
    1.76 - (*     remove_thy"Typefix";
    1.77 - 	use_thy"~/proto2/isac/src/sml/IsacKnowledge/Isac";
    1.78 -        *)
    1.79 - 	cd "..";
    1.80 -"**** build IsacKnowledge complete ***********************";
    1.81 -"**** build isac kernel complete *************************";
    1.82 - 
    1.83 -states:=[];
    1.84 -print_depth 3;