1 (* Title: All tests on isac; observe outcommented
2 Author: Walther Neuper 101001
3 (c) copyright due to lincense terms.
5 $ cd /usr/local/isabisac/test/Tools/isac
6 $ /usr/local/Isabelle/bin/isabelle jedit -l Isac Test_Isac.thy &
7 1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
8 10 20 30 40 50 60 70 80 90 100
11 theory Test_Isac imports
13 OUTCOMMENT THE ABOVE AND SET <Prover Session> <Isac> (INSTEAD OF 'HOL')
15 <Isac> HAS BEEN CREATED BY /usr/local/isabisac/bin/isabelle usedir -b HOL Isac,
16 CREATION SEEMS TO BE CORRECT:
17 $ ls -l "/home/neuper/.isabelle/Isabelle2012/heaps/polyml-5.4.1_x86_64-linux/Isac"
18 -r--r--r-- 1 neuper neuper 296349832 Jun 16 11:41 /home/neuper/.isabelle/Isabelle2012/heaps/polyml-5.4.1_x86_64-linux/Isac
20 (*"Knowledge/Rational_Test" ...THIS FILE HAS DISAPPEARED*)
22 (*CAUSES ERROR: Bad theory (file "/usr/local/isabisac/test/Tools/isac/ADDTESTS/All_Ctxt.thy")
23 ??? HOW CAN I MAKE <Prover Session> <Isac> WORK FOR Test_Isac.thy ??? *)
24 "ADDTESTS/test-depend/Build_Test"
26 "ADDTESTS/course/phst11/T1_Basics"
27 "ADDTESTS/course/phst11/T2_Rewriting"
28 "ADDTESTS/course/phst11/T3_MathEngine"
29 "ADDTESTS/file-depend/Build_Test"
30 "ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
31 "../../Pure/Isar/Test_Parsers"
32 (*"../../Pure/Isar/Pure/Isar/Struct_Deriv" update 2009-2-->2011*)
33 "../../Pure/Isar/Test_Parse_Term"
38 ("ProgLang/termC.sml")
39 ("ProgLang/calculate.sml")
40 ("ProgLang/rewrite.sml")
41 ("ProgLang/listg.sml")
42 ("ProgLang/scrtools.sml")
43 ("ProgLang/tools.sml")
45 ("Minisubpbl/000-comments.sml")
46 ("Minisubpbl/100-init-rootpbl.sml")
47 ("Minisubpbl/150-add-given.sml")
48 ("Minisubpbl/200-start-method.sml")
49 ("Minisubpbl/300-init-subpbl.sml")
50 ("Minisubpbl/400-start-meth-subpbl.sml")
51 ("Minisubpbl/490-nxt-Check_Postcond.sml")
52 ("Minisubpbl/500-met-sub-to-root.sml")
53 ("Minisubpbl/530-error-Check_Elementwise.sml")
54 ("Minisubpbl/600-postcond.sml")
56 ("Interpret/mstools.sml")
57 ("Interpret/ctree.sml")
58 ("Interpret/ptyps.sml")
59 ("Interpret/generate.sml")
60 ("Interpret/calchead.sml")
61 ("Interpret/appl.sml")
62 ("Interpret/rewtools.sml")
63 ("Interpret/script.sml")
64 ("Interpret/solve.sml")
65 ("Interpret/inform.sml")
66 ("Interpret/mathengine.sml")
69 ("xmlsrc/datatypes.sml")
70 ("xmlsrc/pbl-met-hierarchy.sml")
71 ("xmlsrc/thy-hierarchy.sml")
72 ("xmlsrc/interface-xml.sml")
74 ("Frontend/messages.sml")
75 ("Frontend/states.sml")
76 ("Frontend/interface.sml")
79 ("Knowledge/delete.sml")
80 ("Knowledge/descript.sml")
81 ("Knowledge/atools.sml")
82 ("Knowledge/simplify.sml")
83 ("Knowledge/poly.sml")
84 ("Knowledge/rational.sml")
85 ("Knowledge/equation.sml")
86 ("Knowledge/root.sml")
87 ("Knowledge/lineq.sml")
88 ("Knowledge/rooteq.sml")
89 ("Knowledge/rateq.sml")
90 ("Knowledge/rootrateq.sml")
91 ("Knowledge/polyeq.sml")
92 ("Knowledge/calculus.sml")
93 ("Knowledge/trig.sml")
94 ("Knowledge/logexp.sml")
95 ("Knowledge/diff.sml")
96 ("Knowledge/integrate.sml")
97 ("Knowledge/eqsystem.sml")
98 ("Knowledge/test.sml")
99 ("Knowledge/partial_fractions.sml")
100 ("Knowledge/polyminus.sml")
101 ("Knowledge/vect.sml")
102 ("Knowledge/diffapp.sml")
103 ("Knowledge/biegelinie.sml")
104 ("Knowledge/algein.sml")
105 ("Knowledge/diophanteq.sml")
106 ("Knowledge/Inverse_Z_Transform/inverse_z_transform.sml")
107 ("Knowledge/isac.sml")
108 ("Knowledge/build_thydata.sml")
112 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
115 use "ProgLang/termC.sml"
116 use "ProgLang/calculate.sml"
117 use "ProgLang/rewrite.sml"
118 (*use "ProgLang/listC.sml" 2002*)
119 use "ProgLang/scrtools.sml"
120 use "ProgLang/tools.sml"
121 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
122 ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}
123 use "Minisubpbl/000-comments.sml"
124 use "Minisubpbl/100-init-rootpbl.sml"
125 use "Minisubpbl/150-add-given.sml"
126 use "Minisubpbl/200-start-method.sml"
127 use "Minisubpbl/300-init-subpbl.sml"
128 use "Minisubpbl/400-start-meth-subpbl.sml"
129 use "Minisubpbl/490-nxt-Check_Postcond.sml"
130 use "Minisubpbl/500-met-sub-to-root.sml"
131 use "Minisubpbl/530-error-Check_Elementwise.sml"
132 use "Minisubpbl/600-postcond.sml"
133 ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
134 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
135 use "Interpret/mstools.sml"
136 use "Interpret/ctree.sml" (*!...!see(25)*)
137 use "Interpret/ptyps.sml"
138 ML {* check_unsynchronized_ref (); (*========= on error: CUT AND PASTE THIS LINE =========*) *}
139 use "Interpret/generate.sml"
140 use "Interpret/calchead.sml" (*part.*)
141 use "Interpret/appl.sml" (*!complete WEGEN INTERMED TESTCODE*)
142 use "Interpret/rewtools.sml" (*TODO/part.WN120406*)
143 use "Interpret/script.sml" (*!TODO/part.*)
144 use "Interpret/solve.sml" (*part.*)
145 use "Interpret/inform.sml" (*part.*)
146 use "Interpret/mathengine.sml" (*!part.*)
147 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
148 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
149 use "xmlsrc/mathml.sml" (*part.*)
150 use "xmlsrc/datatypes.sml" (*TODO/part.*)
151 use "xmlsrc/pbl-met-hierarchy.sml" (*TODO after 2009-2/part.*)
152 use "xmlsrc/thy-hierarchy.sml" (*TODO after 2009-2/part.*)
153 use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
154 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
155 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
156 use "Frontend/messages.sml"
157 use "Frontend/states.sml"
158 use "Frontend/interface.sml"
159 use "print_exn_G.sml"
160 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
161 ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
162 use "Knowledge/delete.sml"
163 use "Knowledge/descript.sml"
164 use "Knowledge/atools.sml"
165 use "Knowledge/simplify.sml"
166 use "Knowledge/poly.sml"
167 use "Knowledge/gcd_poly_winkler.sml"
168 (*use "Knowledge/rational.sml" WN120317.TODO postponed to joint work with dmeindl *)
169 use "Knowledge/equation.sml"
170 use "Knowledge/root.sml"
171 use "Knowledge/lineq.sml"
172 (*use "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
173 use "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *)
174 use "Knowledge/rootrat.sml"
175 use "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
176 use "Knowledge/partial_fractions.sml"
177 use "Knowledge/polyeq.sml"
178 (*use "Knowledge/rlang.sml" much to clean up, not urgent due to similar tests *)
179 use "Knowledge/calculus.sml"
180 use "Knowledge/trig.sml"
181 (*use "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
182 use "Knowledge/diff.sml"
183 use "Knowledge/integrate.sml"
184 use "Knowledge/eqsystem.sml"
185 use "Knowledge/test.sml"
186 use "Knowledge/polyminus.sml"
187 use "Knowledge/vect.sml"
188 use "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
189 use "Knowledge/biegelinie.sml"
190 use "Knowledge/algein.sml"
191 use "Knowledge/diophanteq.sml"
192 use "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
193 use "Knowledge/isac.sml"
194 use "Knowledge/build_thydata.sml"
195 ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}
196 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
197 ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*}
198 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
201 (*========== inhibit exn 110628 ================================================
202 ============ inhibit exn 110628 ==============================================*)
204 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
205 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)