1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Wed Aug 25 16:20:07 2010 +0200
     1.3 @@ -0,0 +1,103 @@
     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 Build_Isac.thy &
     1.9 +$ /usr/local/isabisac/bin/isabelle jedit Build_Isac.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 Build_Isac
    1.18 +(*imports Complex_Main*)
    1.19 +imports Complex_Main "ProgLang/Script" 
    1.20 +  (*ListC, Tools, Script*)
    1.21 +begin
    1.22 +
    1.23 +ML {* 
    1.24 +writeln "**** build the isac kernel = math-engine + Knowledge ***********";
    1.25 +writeln "**** build the math-engine *************************************" *}
    1.26 +
    1.27 +ML {* Toplevel.debug := true; *}
    1.28 +use "library.sml"
    1.29 +use "calcelems.sml"
    1.30 +ML {* check_guhs_unique := true *}
    1.31 +
    1.32 +use "ProgLang/term.sml"
    1.33 +use "ProgLang/calculate.sml"
    1.34 +use "ProgLang/rewrite.sml"
    1.35 +use_thy"ProgLang/Script"
    1.36 +use "ProgLang/scrtools.sml"
    1.37 +
    1.38 +use "Interpret/mstools.sml"
    1.39 +use "Interpret/ctree.sml"
    1.40 +use "Interpret/ptyps.sml"
    1.41 +use "Interpret/generate.sml"
    1.42 +use "Interpret/calchead.sml"
    1.43 +use "Interpret/appl.sml"
    1.44 +use "Interpret/rewtools.sml"
    1.45 +use "Interpret/script.sml"
    1.46 +use "Interpret/solve.sml"
    1.47 +use "Interpret/inform.sml"
    1.48 +use "Interpret/mathengine.sml"
    1.49 +
    1.50 +use "xmlsrc/mathml.sml"
    1.51 +use "xmlsrc/datatypes.sml"
    1.52 +use "xmlsrc/pbl-met-hierarchy.sml"
    1.53 +use "xmlsrc/thy-hierarchy.sml" 
    1.54 +use "xmlsrc/interface-xml.sml"
    1.55 +
    1.56 +use "Frontend/messages.sml"
    1.57 +use "Frontend/states.sml"
    1.58 +use "Frontend/interface.sml"
    1.59 +
    1.60 +use "print_exn_G.sml"
    1.61 +ML {* writeln "**** build math-engine complete **************************" *}
    1.62 +
    1.63 +ML {* writeln "**** build the Knowledge *********************************" *}
    1.64 +use_thy "Knowledge/Typefix"
    1.65 +use_thy "Knowledge/Descript"
    1.66 +
    1.67 +ML {*
    1.68 +
    1.69 +111;
    1.70 +*}
    1.71 +
    1.72 +use_thy "Knowledge/Atools"
    1.73 +
    1.74 +
    1.75 +ML {*
    1.76 +val str = "1234567890";
    1.77 +*}
    1.78 +
    1.79 +(*
    1.80 +use_thy "Knowledge/Simplify"
    1.81 +use_thy "Knowledge/Poly"
    1.82 +use_thy "Knowledge/Rational"
    1.83 +use_thy "Knowledge/PolyMinus"
    1.84 +use_thy "Knowledge/Equation"
    1.85 +use_thy "Knowledge/LinEq"
    1.86 +use_thy "Knowledge/Root"
    1.87 +use_thy "Knowledge/RootEq"
    1.88 +use_thy "Knowledge/RatEq"
    1.89 +use_thy "Knowledge/RootRat"
    1.90 +use_thy "Knowledge/RootRatEq"
    1.91 +use_thy "Knowledge/PolyEq"
    1.92 +use_thy "Knowledge/Vect"
    1.93 +use_thy "Knowledge/Calculus"
    1.94 +use_thy "Knowledge/Trig"
    1.95 +use_thy "Knowledge/LogExp"
    1.96 +use_thy "Knowledge/Diff"
    1.97 +use_thy "Knowledge/DiffApp"
    1.98 +use_thy "Knowledge/Integrate"
    1.99 +use_thy "Knowledge/EqSystem"
   1.100 +use_thy "Knowledge/Biegelinie"
   1.101 +use_thy "Knowledge/AlgEin"
   1.102 +use_thy "Knowledge/Test"
   1.103 +use_thy "Knowledge/Isac"
   1.104 +*)
   1.105 +end
   1.106 +