1.1 --- a/src/Tools/isac/Isac_Mathengine.thy	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,102 +0,0 @@
     1.4 -(*  Title:   ~~~/isac/Isac_Mathengine.thy
     1.5 -    Author: Walther Neuper, TU Graz
     1.6 -
     1.7 -$ cd /usr/local/Isabelle2009-1/src/Tools/isac
     1.8 -$ /usr/local/isabisac/bin/isabelle emacs Isac_Mathengine.thy &
     1.9 -$ /usr/local/isabisac/bin/isabelle jedit Isac_Mathengine.thy &
    1.10 -
    1.11 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
    1.12 -        10        20        30        40        50        60        70        80
    1.13 -*)
    1.14 -
    1.15 -header {* Loading the isac mathengine *}
    1.16 -
    1.17 -theory Isac_Mathengine
    1.18 -(*imports Complex_Main*)
    1.19 -imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*)
    1.20 -begin
    1.21 -
    1.22 -ML {* 
    1.23 -writeln "**** build the isac kernel = math-engine + IsacKnowledge ";
    1.24 -writeln "**** build the math-engine ******************************" *}
    1.25 -
    1.26 -ML {* Toplevel.debug := true; *}
    1.27 -use "library.sml"
    1.28 -use "calcelems.sml"
    1.29 -ML {* check_guhs_unique := true *}
    1.30 -
    1.31 -use "Scripts/term_G.sml"
    1.32 -use "Scripts/calculate.sml"
    1.33 -use "Scripts/rewrite.sml"
    1.34 -use_thy"Scripts/Script"
    1.35 -use "Scripts/scrtools.sml"
    1.36 -
    1.37 -use "ME/mstools.sml"
    1.38 -use "ME/ctree.sml"
    1.39 -use "ME/ptyps.sml"
    1.40 -use "ME/generate.sml"
    1.41 -use "ME/calchead.sml"
    1.42 -use "ME/appl.sml"
    1.43 -use "ME/rewtools.sml"
    1.44 -use "ME/script.sml"
    1.45 -use "ME/solve.sml"
    1.46 -use "ME/inform.sml"
    1.47 -use "ME/mathengine.sml"
    1.48 -
    1.49 -use "xmlsrc/mathml.sml"
    1.50 -use "xmlsrc/datatypes.sml"
    1.51 -use "xmlsrc/pbl-met-hierarchy.sml"
    1.52 -use "xmlsrc/thy-hierarchy.sml" 
    1.53 -use "xmlsrc/interface-xml.sml"
    1.54 -
    1.55 -use "FE-interface/messages.sml"
    1.56 -use "FE-interface/states.sml"
    1.57 -use "FE-interface/interface.sml"
    1.58 -
    1.59 -use "print_exn_G.sml"
    1.60 -text "**** build math-engine complete *************************"
    1.61 -
    1.62 -ML {* writeln "**** build the IsacKnowledge ****************************" *}
    1.63 -use_thy"IsacKnowledge/Typefix"
    1.64 -use_thy"IsacKnowledge/Descript"
    1.65 -
    1.66 -ML {*
    1.67 -
    1.68 -111;
    1.69 -*}
    1.70 -
    1.71 -use_thy"IsacKnowledge/Atools"
    1.72 -
    1.73 -
    1.74 -ML {*
    1.75 -val str = "1234567890";
    1.76 -*}
    1.77 -
    1.78 -(*
    1.79 -use_thy"IsacKnowledge/Simplify"
    1.80 -use_thy"IsacKnowledge/Poly"
    1.81 -use_thy"IsacKnowledge/Rational"
    1.82 -use_thy"IsacKnowledge/PolyMinus"
    1.83 -use_thy"IsacKnowledge/Equation"
    1.84 -use_thy"IsacKnowledge/LinEq"
    1.85 -use_thy"IsacKnowledge/Root"
    1.86 -use_thy"IsacKnowledge/RootEq"
    1.87 -use_thy"IsacKnowledge/RatEq"
    1.88 -use_thy"IsacKnowledge/RootRat"
    1.89 -use_thy"IsacKnowledge/RootRatEq"
    1.90 -use_thy"IsacKnowledge/PolyEq"
    1.91 -use_thy"IsacKnowledge/Vect"
    1.92 -use_thy"IsacKnowledge/Calculus"
    1.93 -use_thy"IsacKnowledge/Trig"
    1.94 -use_thy"IsacKnowledge/LogExp"
    1.95 -use_thy"IsacKnowledge/Diff"
    1.96 -use_thy"IsacKnowledge/DiffApp"
    1.97 -use_thy"IsacKnowledge/Integrate"
    1.98 -use_thy"IsacKnowledge/EqSystem"
    1.99 -use_thy"IsacKnowledge/Biegelinie"
   1.100 -use_thy"IsacKnowledge/AlgEin"
   1.101 -use_thy"IsacKnowledge/Test"
   1.102 -use_thy"IsacKnowledge/Isac"
   1.103 -*)
   1.104 -end
   1.105 -