author | Walther Neuper <neuper@ist.tugraz.at> |
Wed, 11 May 2011 07:28:13 +0200 | |
branch | decompose-isar |
changeset 41980 | 6ec461ac6c76 |
parent 41979 | 159e5b703965 |
child 41981 | 9e2de17e4071 |
permissions | -rw-r--r-- |
neuper@41945 | 1 |
(* Title: All tests on isac; observe outcommented |
neuper@41943 | 2 |
Author: Walther Neuper 101001 |
neuper@41943 | 3 |
(c) copyright due to lincense terms. |
neuper@41943 | 4 |
|
neuper@41943 | 5 |
$ cd /usr/local/isabisac/test/Tools/isac |
neuper@41978 | 6 |
$ /usr/local/Isabelle/bin/isabelle jedit -l Isac Test_Isac.thy & |
neuper@41968 | 7 |
1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890 |
neuper@41968 | 8 |
10 20 30 40 50 60 70 80 90 100 |
neuper@41943 | 9 |
*) |
neuper@41943 | 10 |
|
neuper@41979 | 11 |
theory Test_Isac imports |
neuper@41979 | 12 |
Isac |
neuper@41979 | 13 |
"Knowledge/Rational_Test" |
neuper@41980 | 14 |
"ADDTESTS/Ctxt" |
neuper@41979 | 15 |
|
neuper@41945 | 16 |
uses |
neuper@41945 | 17 |
( "library.sml") |
neuper@41945 | 18 |
( "calcelems.sml") |
neuper@41945 | 19 |
("ProgLang/termC.sml") |
neuper@41945 | 20 |
("ProgLang/calculate.sml") |
neuper@41945 | 21 |
("ProgLang/rewrite.sml") |
neuper@41945 | 22 |
(*("ProgLang/listg.sml") ("ProgLang/scrtools.sml") ("ProgLang/tools.sml") *) |
neuper@41945 | 23 |
|
neuper@41945 | 24 |
("Interpret/mstools.sml") |
bonzai@41951 | 25 |
("Interpret/ctree.sml") |
neuper@41945 | 26 |
("Interpret/ptyps.sml") |
neuper@41945 | 27 |
(*("Interpret/generate.sml")*) |
neuper@41945 | 28 |
("Interpret/calchead.sml") |
neuper@41945 | 29 |
(*("Interpret/appl.sml")*) |
neuper@41945 | 30 |
("Interpret/rewtools.sml") |
neuper@41945 | 31 |
(*("Interpret/script.sml") |
neuper@41945 | 32 |
("Interpret/solve.sml") |
neuper@41945 | 33 |
("Interpret/inform.sml")*) |
neuper@41945 | 34 |
("Interpret/mathengine.sml") |
neuper@41945 | 35 |
|
neuper@41945 | 36 |
(*("xmlsrc/mathml.sml") |
neuper@41945 | 37 |
("xmlsrc/datatypes.sml") |
neuper@41945 | 38 |
("xmlsrc/pbl-met-hierarchy.sml") |
neuper@41945 | 39 |
("xmlsrc/thy-hierarchy.sml")*) |
neuper@41945 | 40 |
("xmlsrc/interface-xml.sml") |
neuper@41945 | 41 |
|
neuper@41945 | 42 |
("Frontend/messages.sml") |
neuper@41945 | 43 |
("Frontend/states.sml") |
neuper@41945 | 44 |
("Frontend/interface.sml") |
neuper@41945 | 45 |
("print_exn_G.sml") |
neuper@41945 | 46 |
|
neuper@41945 | 47 |
("Knowledge/delete.sml") |
neuper@41945 | 48 |
("Knowledge/descript.sml") |
neuper@41945 | 49 |
("Knowledge/atools.sml") |
neuper@41945 | 50 |
("Knowledge/simplify.sml") |
neuper@41945 | 51 |
("Knowledge/poly.sml") |
neuper@41945 | 52 |
("Knowledge/rational.sml") |
neuper@41945 | 53 |
("Knowledge/equation.sml") |
neuper@41945 | 54 |
("Knowledge/root.sml") |
neuper@41945 | 55 |
("Knowledge/lineq.sml") |
neuper@41945 | 56 |
("Knowledge/rooteq.sml") |
neuper@41945 | 57 |
("Knowledge/rateq.sml") |
neuper@41945 | 58 |
("Knowledge/rootrateq.sml") |
neuper@41945 | 59 |
(*("Knowledge/polyeq.sml")*) |
neuper@41945 | 60 |
("Knowledge/calculus.sml") |
neuper@41945 | 61 |
("Knowledge/trig.sml") |
neuper@41945 | 62 |
("Knowledge/logexp.sml") |
neuper@41945 | 63 |
("Knowledge/diff.sml") |
neuper@41945 | 64 |
("Knowledge/integrate.sml") |
neuper@41945 | 65 |
("Knowledge/eqsystem.sml") |
neuper@41945 | 66 |
("Knowledge/test.sml") |
neuper@41945 | 67 |
("Knowledge/polyminus.sml") |
neuper@41945 | 68 |
("Knowledge/vect.sml") |
neuper@41945 | 69 |
("Knowledge/diffapp.sml") |
neuper@41945 | 70 |
("Knowledge/biegelinie.sml") |
neuper@41945 | 71 |
("Knowledge/algein.sml") |
neuper@41945 | 72 |
("Knowledge/diophanteq.sml") |
neuper@41945 | 73 |
("Knowledge/isac.sml") |
neuper@41945 | 74 |
|
neuper@41943 | 75 |
begin |
neuper@41947 | 76 |
|
neuper@41943 | 77 |
ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*} |
neuper@41945 | 78 |
use "library.sml" (*new 2011*) |
neuper@41945 | 79 |
use "calcelems.sml" (*complete*) |
neuper@41943 | 80 |
use "ProgLang/termC.sml" (*part.*) |
neuper@41943 | 81 |
use "ProgLang/calculate.sml" (*part.*) |
neuper@41943 | 82 |
use "ProgLang/rewrite.sml" (*part.*) |
neuper@41943 | 83 |
(*use "ProgLang/listg.sml" 2002*) |
neuper@41943 | 84 |
(*use "ProgLang/scrtools.sml" 2002*) |
neuper@41943 | 85 |
(*use "ProgLang/tools.sml" 2002*) |
neuper@41943 | 86 |
ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*} |
neuper@41943 | 87 |
ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*} |
neuper@41973 | 88 |
ML {* |
neuper@41976 | 89 |
*} |
neuper@41976 | 90 |
|
neuper@41975 | 91 |
use "Interpret/mstools.sml" (*new 2010*) |
neuper@41975 | 92 |
use "Interpret/ctree.sml" (*!...see(25)*) |
neuper@41943 | 93 |
use "Interpret/ptyps.sml" (* *) |
neuper@41943 | 94 |
(*use "Interpret/generate.sml" new 2011*) |
neuper@41972 | 95 |
use "Interpret/calchead.sml" (*! *) |
neuper@41975 | 96 |
use "Interpret/appl.sml" (*!complete WEGEN INTERMED TESTCODE*) |
neuper@41972 | 97 |
use "Interpret/rewtools.sml" (*! *) |
neuper@41972 | 98 |
use "Interpret/script.sml" (*!TODO*) |
neuper@41972 | 99 |
(*use "Interpret/solve.sml" !TODO*) |
neuper@41972 | 100 |
(*use "Interpret/inform.sml" !TODO*) |
neuper@41972 | 101 |
use "Interpret/mathengine.sml" (*!part.*) |
neuper@41943 | 102 |
ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*} |
neuper@41943 | 103 |
ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*} |
neuper@41943 | 104 |
(*use "xmlsrc/mathml.sml" TODO*) |
neuper@41943 | 105 |
(*use "xmlsrc/datatypes.sml" TODO*) |
neuper@41943 | 106 |
(*use "xmlsrc/pbl-met-hierarchy.sml" TODO*) |
neuper@41943 | 107 |
(*use "xmlsrc/thy-hierarchy.sml" TODO after 2009-2*) |
neuper@41943 | 108 |
use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*) |
neuper@41943 | 109 |
ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*} |
neuper@41943 | 110 |
ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*} |
neuper@41943 | 111 |
use "Frontend/messages.sml" (*new 2011*) |
neuper@41943 | 112 |
use "Frontend/states.sml" (*new 2011*) |
neuper@41945 | 113 |
use "Frontend/interface.sml" (*part.*) |
neuper@41945 | 114 |
use "print_exn_G.sml" (*new 2011*) |
neuper@41943 | 115 |
ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*} |
neuper@41943 | 116 |
ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*} |
neuper@41943 | 117 |
use "Knowledge/delete.sml" (*new 2011*) |
neuper@41943 | 118 |
use "Knowledge/descript.sml" (*new 2011*) |
neuper@41943 | 119 |
(*use "Knowledge/atools.sml" 2002, added termorder.sml 2011*) |
neuper@41943 | 120 |
use "Knowledge/simplify.sml" (*part.*) |
neuper@41943 | 121 |
(*use "Knowledge/poly.sml" 2002*) |
neuper@41947 | 122 |
(*use "Knowledge/rational.sml" part.; diff.emacs--jedit*) |
neuper@41943 | 123 |
(*use "Knowledge/equation.sml" 2002*) |
neuper@41943 | 124 |
(*use "Knowledge/root.sml" 2002*) |
neuper@41943 | 125 |
use "Knowledge/lineq.sml" (*new 2011*) |
neuper@41943 | 126 |
(*use "Knowledge/rooteq.sml" 2002*) |
neuper@41943 | 127 |
(*use "Knowledge/rateq.sml" 2002*) |
neuper@41943 | 128 |
(*use "Knowledge/rootrat.sml" 2002*) |
neuper@41943 | 129 |
(*use "Knowledge/rootrateq.sml" 2002*) |
neuper@41943 | 130 |
(*use "Knowledge/polyeq.sml" 2002*) |
neuper@41956 | 131 |
(*use "Knowledge/rlang.sml" 2002???*) |
neuper@41943 | 132 |
use "Knowledge/calculus.sml" (*new 2011*) |
neuper@41943 | 133 |
(*use "Knowledge/trig.sml" 2002*) |
neuper@41943 | 134 |
(*use "Knowledge/logexp.sml" 2002*) |
neuper@41943 | 135 |
use "Knowledge/diff.sml" (*part.*) |
neuper@41947 | 136 |
(*use "Knowledge/integrate.sml" part. was complete 2009-2 |
neuper@41947 | 137 |
diff.emacs--jedit*) |
neuper@41943 | 138 |
(*use "Knowledge/eqsystem.sml" 2002*) |
neuper@41943 | 139 |
use "Knowledge/test.sml" (*new 2011*) |
neuper@41943 | 140 |
use "Knowledge/polyminus.sml" (*part.*) |
neuper@41943 | 141 |
(*use "Knowledge/vect.sml" 2002*) |
neuper@41943 | 142 |
(*use "Knowledge/diffapp.sml" 2002*) |
neuper@41943 | 143 |
(*use "Knowledge/biegelinie.sml" 2002*) |
neuper@41943 | 144 |
(*use "Knowledge/algein.sml" 2002*) |
neuper@41943 | 145 |
use "Knowledge/diophanteq.sml" (*complete*) |
neuper@41943 | 146 |
use "Knowledge/isac.sml" (*part.*) |
neuper@41943 | 147 |
ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*} |
neuper@41945 | 148 |
ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} |
neuper@41945 | 149 |
ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*} |
neuper@41945 | 150 |
ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} |
neuper@41943 | 151 |
|
neuper@41943 | 152 |
end |
neuper@41943 | 153 |
|
neuper@41943 | 154 |
(*=== inhibit exn ?============================================================= |
neuper@41943 | 155 |
===== inhibit exn ?===========================================================*) |
neuper@41943 | 156 |
|
neuper@41969 | 157 |
(*========== inhibit exn 110503 ================================================ |
neuper@41943 | 158 |
|
neuper@41943 | 159 |
"########### testcode inserted vvv ###########################################"; |
neuper@41943 | 160 |
"########### testcode inserted ^^^ ###########################################"; |
neuper@41943 | 161 |
|
neuper@41969 | 162 |
============ inhibit exn 110503 ==============================================*) |
neuper@41943 | 163 |
|
neuper@41943 | 164 |
(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
neuper@41943 | 165 |
-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) |
neuper@41975 | 166 |