Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Build_Isac.thy
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 25 Aug 2010 16:49:56 +0200
branchisac-update-Isa09-2
changeset 37948 ed85f172569c
parent 37947 22235e4dbe5f
child 37949 aaf528d3ebd5
permissions -rw-r--r--
stuck at Atools.thy again; resume test on dependencies 
     1 (*  Title:   ~~~/isac/Isac_Mathengine.thy

     2     Author: Walther Neuper, TU Graz

     3 

     4 $ cd /usr/local/Isabelle2009-1/src/Tools/isac

     5 $ /usr/local/isabisac/bin/isabelle emacs Build_Isac.thy &

     6 $ /usr/local/isabisac/bin/isabelle jedit Build_Isac.thy &

     7 

     8 12345678901234567890123456789012345678901234567890123456789012345678901234567890

     9         10        20        30        40        50        60        70        80

    10 *)

    11 

    12 header {* Loading the isac mathengine *}

    13 

    14 theory Build_Isac

    15 (*imports Complex_Main*)

    16 imports Complex_Main "ProgLang/Script" 

    17   (*ListC, Tools, Script*)

    18 begin

    19 

    20 ML {* 

    21 writeln "**** build the isac kernel = math-engine + Knowledge ***********";

    22 writeln "**** build the math-engine *************************************" *}

    23 

    24 ML {* Toplevel.debug := true; *}

    25 use "library.sml"

    26 use "calcelems.sml"

    27 ML {* check_guhs_unique := true *}

    28 

    29 use "ProgLang/term.sml"

    30 use "ProgLang/calculate.sml"

    31 use "ProgLang/rewrite.sml"

    32 use_thy"ProgLang/Script"

    33 use "ProgLang/scrtools.sml"

    34 

    35 use "Interpret/mstools.sml"

    36 use "Interpret/ctree.sml"

    37 use "Interpret/ptyps.sml"

    38 use "Interpret/generate.sml"

    39 use "Interpret/calchead.sml"

    40 use "Interpret/appl.sml"

    41 use "Interpret/rewtools.sml"

    42 use "Interpret/script.sml"

    43 use "Interpret/solve.sml"

    44 use "Interpret/inform.sml"

    45 use "Interpret/mathengine.sml"

    46 

    47 use "xmlsrc/mathml.sml"

    48 use "xmlsrc/datatypes.sml"

    49 use "xmlsrc/pbl-met-hierarchy.sml"

    50 use "xmlsrc/thy-hierarchy.sml" 

    51 use "xmlsrc/interface-xml.sml"

    52 

    53 use "Frontend/messages.sml"

    54 use "Frontend/states.sml"

    55 use "Frontend/interface.sml"

    56 

    57 use "print_exn_G.sml"

    58 ML {* writeln "**** build math-engine complete **************************" *}

    59 

    60 ML {* writeln "**** build the Knowledge *********************************" *}

    61 use_thy "Knowledge/Typefix"

    62 use_thy "Knowledge/Descript"

    63 

    64 use_thy "Knowledge/Atools"

    65 

    66 

    67 ML {*

    68 111;

    69 *}

    70 

    71 (*

    72 use_thy "Knowledge/Simplify"

    73 use_thy "Knowledge/Poly"

    74 use_thy "Knowledge/Rational"

    75 use_thy "Knowledge/PolyMinus"

    76 use_thy "Knowledge/Equation"

    77 use_thy "Knowledge/LinEq"

    78 use_thy "Knowledge/Root"

    79 use_thy "Knowledge/RootEq"

    80 use_thy "Knowledge/RatEq"

    81 use_thy "Knowledge/RootRat"

    82 use_thy "Knowledge/RootRatEq"

    83 use_thy "Knowledge/PolyEq"

    84 use_thy "Knowledge/Vect"

    85 use_thy "Knowledge/Calculus"

    86 use_thy "Knowledge/Trig"

    87 use_thy "Knowledge/LogExp"

    88 use_thy "Knowledge/Diff"

    89 use_thy "Knowledge/DiffApp"

    90 use_thy "Knowledge/Integrate"

    91 use_thy "Knowledge/EqSystem"

    92 use_thy "Knowledge/Biegelinie"

    93 use_thy "Knowledge/AlgEin"

    94 use_thy "Knowledge/Test"

    95 use_thy "Knowledge/Isac"

    96 *)

    97 end

    98
wneuper/isa