diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/Build_Isac.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Build_Isac.thy	Wed Aug 25 16:20:07 2010 +0200
@@ -0,0 +1,103 @@
+(*  Title:   ~~~/isac/Isac_Mathengine.thy
+    Author: Walther Neuper, TU Graz
+
+$ cd /usr/local/Isabelle2009-1/src/Tools/isac
+$ /usr/local/isabisac/bin/isabelle emacs Build_Isac.thy &
+$ /usr/local/isabisac/bin/isabelle jedit Build_Isac.thy &
+
+12345678901234567890123456789012345678901234567890123456789012345678901234567890
+        10        20        30        40        50        60        70        80
+*)
+
+header {* Loading the isac mathengine *}
+
+theory Build_Isac
+(*imports Complex_Main*)
+imports Complex_Main "ProgLang/Script" 
+  (*ListC, Tools, Script*)
+begin
+
+ML {* 
+writeln "**** build the isac kernel = math-engine + Knowledge ***********";
+writeln "**** build the math-engine *************************************" *}
+
+ML {* Toplevel.debug := true; *}
+use "library.sml"
+use "calcelems.sml"
+ML {* check_guhs_unique := true *}
+
+use "ProgLang/term.sml"
+use "ProgLang/calculate.sml"
+use "ProgLang/rewrite.sml"
+use_thy"ProgLang/Script"
+use "ProgLang/scrtools.sml"
+
+use "Interpret/mstools.sml"
+use "Interpret/ctree.sml"
+use "Interpret/ptyps.sml"
+use "Interpret/generate.sml"
+use "Interpret/calchead.sml"
+use "Interpret/appl.sml"
+use "Interpret/rewtools.sml"
+use "Interpret/script.sml"
+use "Interpret/solve.sml"
+use "Interpret/inform.sml"
+use "Interpret/mathengine.sml"
+
+use "xmlsrc/mathml.sml"
+use "xmlsrc/datatypes.sml"
+use "xmlsrc/pbl-met-hierarchy.sml"
+use "xmlsrc/thy-hierarchy.sml" 
+use "xmlsrc/interface-xml.sml"
+
+use "Frontend/messages.sml"
+use "Frontend/states.sml"
+use "Frontend/interface.sml"
+
+use "print_exn_G.sml"
+ML {* writeln "**** build math-engine complete **************************" *}
+
+ML {* writeln "**** build the Knowledge *********************************" *}
+use_thy "Knowledge/Typefix"
+use_thy "Knowledge/Descript"
+
+ML {*
+
+111;
+*}
+
+use_thy "Knowledge/Atools"
+
+
+ML {*
+val str = "1234567890";
+*}
+
+(*
+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/Test"
+use_thy "Knowledge/Isac"
+*)
+end
+