1.1 --- a/src/Tools/isac/Build_Isac.thy	Fri Sep 10 12:15:18 2010 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Mon Sep 13 15:42:03 2010 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  header {* Loading the isac mathengine *}
     1.5  
     1.6  theory Build_Isac
     1.7 -imports Complex_Main "ProgLang/Script" "ProgLang/Language" 
     1.8 +imports Complex_Main "ProgLang/Language" 
     1.9  begin
    1.10  
    1.11  ML {* 
    1.12 @@ -57,33 +57,32 @@
    1.13  ML {* writeln "**** build math-engine complete **************************" *}
    1.14  
    1.15  ML {* writeln "**** build the Knowledge *********************************" *}
    1.16 -(*use_thy "Knowledge/Typefix"*)
    1.17  (*use_thy "Knowledge/Delete"
    1.18    use_thy "Knowledge/Descript"
    1.19    use_thy "Knowledge/Atools"
    1.20    use_thy "Knowledge/Simplify"
    1.21    use_thy "Knowledge/Poly"
    1.22 +  use_thy "Knowledge/Rational"
    1.23 +  use_thy "Knowledge/PolyMinus"
    1.24 +  use_thy "Knowledge/Equation"
    1.25 +  use_thy "Knowledge/LinEq"
    1.26 +  use_thy "Knowledge/Root"
    1.27 +  use_thy "Knowledge/RootEq"
    1.28 +  use_thy "Knowledge/RatEq"
    1.29 +  use_thy "Knowledge/RootRat"
    1.30 +  use_thy "Knowledge/RootRatEq"
    1.31 +  use_thy "Knowledge/PolyEq"
    1.32 +  use_thy "Knowledge/Vect"
    1.33 +  use_thy "Knowledge/Calculus"
    1.34 +  use_thy "Knowledge/Trig"
    1.35 +  use_thy "Knowledge/LogExp"
    1.36 +  use_thy "Knowledge/Diff"
    1.37 +  use_thy "Knowledge/DiffApp"
    1.38 +  use_thy "Knowledge/Integrate"
    1.39 +  use_thy "Knowledge/EqSystem"
    1.40 +  use_thy "Knowledge/Biegelinie"
    1.41 +  use_thy "Knowledge/AlgEin"
    1.42  *)
    1.43 -use_thy "Knowledge/Rational"
    1.44 -use_thy "Knowledge/PolyMinus"
    1.45 -use_thy "Knowledge/Equation"
    1.46 -use_thy "Knowledge/LinEq"
    1.47 -use_thy "Knowledge/Root"
    1.48 -use_thy "Knowledge/RootEq"
    1.49 -use_thy "Knowledge/RatEq"
    1.50 -use_thy "Knowledge/RootRat"
    1.51 -use_thy "Knowledge/RootRatEq"
    1.52 -use_thy "Knowledge/PolyEq"
    1.53 -use_thy "Knowledge/Vect"
    1.54 -use_thy "Knowledge/Calculus"
    1.55 -use_thy "Knowledge/Trig"
    1.56 -use_thy "Knowledge/LogExp"
    1.57 -use_thy "Knowledge/Diff"
    1.58 -use_thy "Knowledge/DiffApp"
    1.59 -use_thy "Knowledge/Integrate"
    1.60 -use_thy "Knowledge/EqSystem"
    1.61 -use_thy "Knowledge/Biegelinie"
    1.62 -use_thy "Knowledge/AlgEin"
    1.63  use_thy "Knowledge/Test"
    1.64  
    1.65  ML {* 111;

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Tools/isac/ROOT.ML	Mon Sep 13 15:42:03 2010 +0200
     2.3 @@ -0,0 +1,7 @@
     2.4 +(*
     2.5 +$ cd /usr/local/Isabelle2009-1/src/Tools/isac
     2.6 +$ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac
     2.7 +
     2.8 +*)
     2.9 +
    2.10 +use_thys ["Build_Isac"];