| author | Walther Neuper <neuper@ist.tugraz.at> |
| Tue, 01 Mar 2011 15:23:59 +0100 | |
| branch | decompose-isar |
| changeset 41905 | b772eb34c16c |
| parent 41900 | 8391d3789efb |
| child 41918 | 7e44a163ac1d |
| permissions | -rw-r--r-- |
| neuper@38070 | 1 |
(* Title: build and test isac |
| neuper@38057 | 2 |
Author: Walther Neuper, TU Graz, 100808 |
| neuper@38051 | 3 |
(c) due to copyright terms |
| neuper@38051 | 4 |
|
| neuper@37910 | 5 |
$ cd /usr/local/Isabelle2009-1/src/Tools/isac |
| neuper@37947 | 6 |
$ /usr/local/isabisac/bin/isabelle emacs Build_Isac.thy & |
| neuper@37947 | 7 |
$ /usr/local/isabisac/bin/isabelle jedit Build_Isac.thy & |
| neuper@37906 | 8 |
|
| neuper@38057 | 9 |
create a new Isac heap (via ~~/ROOT.ML) with |
| neuper@38057 | 10 |
$ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac |
| neuper@38057 | 11 |
|
| neuper@38063 | 12 |
start with Isac |
| neuper@38063 | 13 |
$ /usr/local/isabisac/bin/isabelle emacs -l Isac Build_Isac.thy & |
| neuper@38063 | 14 |
$ /usr/local/isabisac/bin/isabelle jedit -l Isac Build_Isac.thy & |
| neuper@38063 | 15 |
|
| neuper@37924 | 16 |
12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
| neuper@37924 | 17 |
10 20 30 40 50 60 70 80 |
| neuper@37906 | 18 |
*) |
| neuper@37906 | 19 |
|
| neuper@37906 | 20 |
header {* Loading the isac mathengine *}
|
| neuper@37906 | 21 |
|
| neuper@41905 | 22 |
theory Build_Isac imports Complex_Main |
| neuper@41905 | 23 |
(* use "library.sml" |
| neuper@41905 | 24 |
use "calcelems.sml" |
| neuper@41905 | 25 |
|
| neuper@41905 | 26 |
use "ProgLang/termC.sml" |
| neuper@41905 | 27 |
use "ProgLang/calculate.sml" |
| neuper@41905 | 28 |
use "ProgLang/rewrite.sml" |
| neuper@41905 | 29 |
"use_thy ProgLang/ListC" |
| neuper@41905 | 30 |
"use_thy ProgLang/Tools" |
| neuper@41905 | 31 |
"use_thy ProgLang/Script" |
| neuper@41905 | 32 |
use "ProgLang/scrtools.sml" |
| neuper@41905 | 33 |
*) "ProgLang/Language" |
| neuper@41905 | 34 |
|
| neuper@41905 | 35 |
(* use "Interpret/mstools.sml" |
| neuper@41905 | 36 |
use "Interpret/ctree.sml" |
| neuper@41905 | 37 |
use "Interpret/ptyps.sml" |
| neuper@41905 | 38 |
use "Interpret/generate.sml" |
| neuper@41905 | 39 |
use "Interpret/calchead.sml" |
| neuper@41905 | 40 |
use "Interpret/appl.sml" |
| neuper@41905 | 41 |
use "Interpret/rewtools.sml" |
| neuper@41905 | 42 |
use "Interpret/script.sml" |
| neuper@41905 | 43 |
use "Interpret/solve.sml" |
| neuper@41905 | 44 |
use "Interpret/inform.sml" |
| neuper@41905 | 45 |
use "Interpret/mathengine.sml" |
| neuper@41905 | 46 |
*) "Interpret/Interpret" |
| neuper@41905 | 47 |
|
| neuper@41905 | 48 |
(* use "xmlsrc/mathml.sml" |
| neuper@41905 | 49 |
use "xmlsrc/datatypes.sml" |
| neuper@41905 | 50 |
use "xmlsrc/pbl-met-hierarchy.sml" |
| neuper@41905 | 51 |
use "xmlsrc/thy-hierarchy.sml" |
| neuper@41905 | 52 |
use "xmlsrc/interface-xml.sml" |
| neuper@41905 | 53 |
*) "xmlsrc/xmlsrc" |
| neuper@41905 | 54 |
|
| neuper@41905 | 55 |
(* use "Frontend/messages.sml" |
| neuper@41905 | 56 |
use "Frontend/states.sml" |
| neuper@41905 | 57 |
use "Frontend/interface.sml" |
| neuper@41905 | 58 |
|
| neuper@41905 | 59 |
use "print_exn_G.sml" |
| neuper@41905 | 60 |
*) "Frontend/Frontend" |
| neuper@37906 | 61 |
begin |
| neuper@41905 | 62 |
ML {* is_reall_dsc; (*from "ProgLang/scrtools.sml" *) *}
|
| neuper@41905 | 63 |
ML {* me; (*from "Interpret/mathengine.sml"*) *}
|
| neuper@41905 | 64 |
ML {* contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*) *}
|
| neuper@41905 | 65 |
ML {* print_exn_unit *}
|
| neuper@41905 | 66 |
ML {*1*}
|
| neuper@37906 | 67 |
|
| neuper@38015 | 68 |
ML {* tracing "**** build the Knowledge *********************************" *}
|
| neuper@41905 | 69 |
(**) |
| neuper@41905 | 70 |
use_thy "Knowledge/Delete" |
| neuper@37979 | 71 |
use_thy "Knowledge/Descript" |
| neuper@37979 | 72 |
use_thy "Knowledge/Atools" |
| neuper@41905 | 73 |
ML {* list_rls (*from Atools.thy*) *}
|
| neuper@41905 | 74 |
ML {* eval_occurs_in (*from Atools.thy*) *}
|
| neuper@41905 | 75 |
ML {* @{thm last_thmI} (*from Atools.thy*) *}
|
| neuper@41905 | 76 |
|
| neuper@37979 | 77 |
use_thy "Knowledge/Simplify" |
| neuper@37979 | 78 |
use_thy "Knowledge/Poly" |
| neuper@38004 | 79 |
use_thy "Knowledge/Rational" |
| neuper@38004 | 80 |
use_thy "Knowledge/PolyMinus" |
| neuper@38004 | 81 |
use_thy "Knowledge/Equation" |
| neuper@38004 | 82 |
use_thy "Knowledge/LinEq" |
| neuper@38004 | 83 |
use_thy "Knowledge/Root" |
| neuper@38004 | 84 |
use_thy "Knowledge/RootEq" |
| neuper@38004 | 85 |
use_thy "Knowledge/RatEq" |
| neuper@38004 | 86 |
use_thy "Knowledge/RootRat" |
| neuper@38004 | 87 |
use_thy "Knowledge/RootRatEq" |
| neuper@38004 | 88 |
use_thy "Knowledge/PolyEq" |
| neuper@38004 | 89 |
use_thy "Knowledge/Vect" |
| neuper@38004 | 90 |
use_thy "Knowledge/Calculus" |
| neuper@38004 | 91 |
use_thy "Knowledge/Trig" |
| neuper@38004 | 92 |
use_thy "Knowledge/LogExp" |
| neuper@38004 | 93 |
use_thy "Knowledge/Diff" |
| neuper@38004 | 94 |
use_thy "Knowledge/DiffApp" |
| neuper@38004 | 95 |
use_thy "Knowledge/Integrate" |
| neuper@38004 | 96 |
use_thy "Knowledge/EqSystem" |
| neuper@38004 | 97 |
use_thy "Knowledge/Biegelinie" |
| neuper@38004 | 98 |
use_thy "Knowledge/AlgEin" |
| neuper@41905 | 99 |
|
| neuper@41905 | 100 |
ML {*
|
| neuper@41905 | 101 |
@{thm Querkraft_Belastung}
|
| neuper@41905 | 102 |
*} |
| neuper@41905 | 103 |
|
| neuper@38010 | 104 |
use_thy "Knowledge/Test" (*required _only_ for ROOT.ML !?!*) |
| neuper@38005 | 105 |
use_thy "Knowledge/Isac" |
| neuper@38057 | 106 |
|
| neuper@38009 | 107 |
ML {* check_guhs_unique := false; *}
|
| neuper@38015 | 108 |
ML {* tracing "**** isac kernel = math-engine + Knowledge complete ******" *}
|
| neuper@38005 | 109 |
|
| neuper@37906 | 110 |
end |
| neuper@37906 | 111 |
|
| neuper@38057 | 112 |
(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
| neuper@38057 | 113 |
-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) |