# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1284385323 -7200
# Node ID 59caaeeb9afc8aa4cc38f8d908912591818e0e8b
# Parent  0c3e2329eb5ff50bc9928fcaa4df54270769af52
added src/Tools/isac/ROOT.ML

diff -r 0c3e2329eb5f -r 59caaeeb9afc src/Tools/isac/Build_Isac.thy
--- a/src/Tools/isac/Build_Isac.thy	Fri Sep 10 12:15:18 2010 +0200
+++ b/src/Tools/isac/Build_Isac.thy	Mon Sep 13 15:42:03 2010 +0200
@@ -12,7 +12,7 @@
 header {* Loading the isac mathengine *}
 
 theory Build_Isac
-imports Complex_Main "ProgLang/Script" "ProgLang/Language" 
+imports Complex_Main "ProgLang/Language" 
 begin
 
 ML {* 
@@ -57,33 +57,32 @@
 ML {* writeln "**** build math-engine complete **************************" *}
 
 ML {* writeln "**** build the Knowledge *********************************" *}
-(*use_thy "Knowledge/Typefix"*)
 (*use_thy "Knowledge/Delete"
   use_thy "Knowledge/Descript"
   use_thy "Knowledge/Atools"
   use_thy "Knowledge/Simplify"
   use_thy "Knowledge/Poly"
+  use_thy "Knowledge/Rational"
+  use_thy "Knowledge/PolyMinus"
+  use_thy "Knowledge/Equation"
+  use_thy "Knowledge/LinEq"
+  use_thy "Knowledge/Root"
+  use_thy "Knowledge/RootEq"
+  use_thy "Knowledge/RatEq"
+  use_thy "Knowledge/RootRat"
+  use_thy "Knowledge/RootRatEq"
+  use_thy "Knowledge/PolyEq"
+  use_thy "Knowledge/Vect"
+  use_thy "Knowledge/Calculus"
+  use_thy "Knowledge/Trig"
+  use_thy "Knowledge/LogExp"
+  use_thy "Knowledge/Diff"
+  use_thy "Knowledge/DiffApp"
+  use_thy "Knowledge/Integrate"
+  use_thy "Knowledge/EqSystem"
+  use_thy "Knowledge/Biegelinie"
+  use_thy "Knowledge/AlgEin"
 *)
-use_thy "Knowledge/Rational"
-use_thy "Knowledge/PolyMinus"
-use_thy "Knowledge/Equation"
-use_thy "Knowledge/LinEq"
-use_thy "Knowledge/Root"
-use_thy "Knowledge/RootEq"
-use_thy "Knowledge/RatEq"
-use_thy "Knowledge/RootRat"
-use_thy "Knowledge/RootRatEq"
-use_thy "Knowledge/PolyEq"
-use_thy "Knowledge/Vect"
-use_thy "Knowledge/Calculus"
-use_thy "Knowledge/Trig"
-use_thy "Knowledge/LogExp"
-use_thy "Knowledge/Diff"
-use_thy "Knowledge/DiffApp"
-use_thy "Knowledge/Integrate"
-use_thy "Knowledge/EqSystem"
-use_thy "Knowledge/Biegelinie"
-use_thy "Knowledge/AlgEin"
 use_thy "Knowledge/Test"
 
 ML {* 111;
diff -r 0c3e2329eb5f -r 59caaeeb9afc src/Tools/isac/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/ROOT.ML	Mon Sep 13 15:42:03 2010 +0200
@@ -0,0 +1,7 @@
+(*
+$ cd /usr/local/Isabelle2009-1/src/Tools/isac
+$ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac
+
+*)
+
+use_thys ["Build_Isac"];