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/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy &
7 1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
8 10 20 30 40 50 60 70 80 90 100
11 theory Test_Isac imports Isac
15 ("ProgLang/termC.sml")
16 ("ProgLang/calculate.sml")
17 ("ProgLang/rewrite.sml")
18 (*("ProgLang/listg.sml") ("ProgLang/scrtools.sml") ("ProgLang/tools.sml") *)
20 ("Interpret/mstools.sml")
21 ("Interpret/ctree.sml")
22 ("Interpret/ptyps.sml")
23 (*("Interpret/generate.sml")*)
24 ("Interpret/calchead.sml")
25 (*("Interpret/appl.sml")*)
26 ("Interpret/rewtools.sml")
27 (*("Interpret/script.sml")
28 ("Interpret/solve.sml")
29 ("Interpret/inform.sml")*)
30 ("Interpret/mathengine.sml")
32 (*("xmlsrc/mathml.sml")
33 ("xmlsrc/datatypes.sml")
34 ("xmlsrc/pbl-met-hierarchy.sml")
35 ("xmlsrc/thy-hierarchy.sml")*)
36 ("xmlsrc/interface-xml.sml")
38 ("Frontend/messages.sml")
39 ("Frontend/states.sml")
40 ("Frontend/interface.sml")
43 ("Knowledge/delete.sml")
44 ("Knowledge/descript.sml")
45 ("Knowledge/atools.sml")
46 ("Knowledge/simplify.sml")
47 ("Knowledge/poly.sml")
48 ("Knowledge/rational.sml")
49 ("Knowledge/equation.sml")
50 ("Knowledge/root.sml")
51 ("Knowledge/lineq.sml")
52 ("Knowledge/rooteq.sml")
53 ("Knowledge/rateq.sml")
54 ("Knowledge/rootrateq.sml")
55 (*("Knowledge/polyeq.sml")*)
56 ("Knowledge/calculus.sml")
57 ("Knowledge/trig.sml")
58 ("Knowledge/logexp.sml")
59 ("Knowledge/diff.sml")
60 ("Knowledge/integrate.sml")
61 ("Knowledge/eqsystem.sml")
62 ("Knowledge/test.sml")
63 ("Knowledge/polyminus.sml")
64 ("Knowledge/vect.sml")
65 ("Knowledge/diffapp.sml")
66 ("Knowledge/biegelinie.sml")
67 ("Knowledge/algein.sml")
68 ("Knowledge/diophanteq.sml")
69 ("Knowledge/isac.sml")
73 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
74 use "library.sml" (*new 2011*)
75 use "calcelems.sml" (*complete*)
76 use "ProgLang/termC.sml" (*part.*)
77 use "ProgLang/calculate.sml" (*part.*)
78 use "ProgLang/rewrite.sml" (*part.*)
79 (*use "ProgLang/listg.sml" 2002*)
80 (*use "ProgLang/scrtools.sml" 2002*)
81 (*use "ProgLang/tools.sml" 2002*)
82 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
83 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
84 use "Interpret/mstools.sml" (*empty*)
85 use "Interpret/ctree.sml"
86 use "Interpret/ptyps.sml" (* *)
87 (*use "Interpret/generate.sml" new 2011*)
88 use "Interpret/calchead.sml" (* *)
89 (*use "Interpret/appl.sml" new 2011*)
90 use "Interpret/rewtools.sml" (* *)
91 use "Interpret/script.sml" (*TODO*)
92 (*use "Interpret/solve.sml" TODO*)
93 (*use "Interpret/inform.sml" TODO*)
94 use "Interpret/mathengine.sml"(*part.*)
95 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
96 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
97 (*use "xmlsrc/mathml.sml" TODO*)
98 (*use "xmlsrc/datatypes.sml" TODO*)
99 (*use "xmlsrc/pbl-met-hierarchy.sml" TODO*)
100 (*use "xmlsrc/thy-hierarchy.sml" TODO after 2009-2*)
101 use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
102 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
103 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
104 use "Frontend/messages.sml" (*new 2011*)
105 use "Frontend/states.sml" (*new 2011*)
106 use "Frontend/interface.sml" (*part.*)
107 use "print_exn_G.sml" (*new 2011*)
108 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
109 ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
110 use "Knowledge/delete.sml" (*new 2011*)
111 use "Knowledge/descript.sml" (*new 2011*)
112 (*use "Knowledge/atools.sml" 2002, added termorder.sml 2011*)
113 use "Knowledge/simplify.sml" (*part.*)
114 (*use "Knowledge/poly.sml" 2002*)
115 (*use "Knowledge/rational.sml" part.; diff.emacs--jedit*)
116 (*use "Knowledge/equation.sml" 2002*)
117 (*use "Knowledge/root.sml" 2002*)
118 use "Knowledge/lineq.sml" (*new 2011*)
119 (*use "Knowledge/rooteq.sml" 2002*)
120 (*use "Knowledge/rateq.sml" 2002*)
121 (*use "Knowledge/rootrat.sml" 2002*)
122 (*use "Knowledge/rootrateq.sml" 2002*)
123 (*use "Knowledge/polyeq.sml" 2002*)
124 (*use "Knowledge/rlang.sml" 2002???*)
125 use "Knowledge/calculus.sml" (*new 2011*)
126 (*use "Knowledge/trig.sml" 2002*)
127 (*use "Knowledge/logexp.sml" 2002*)
128 use "Knowledge/diff.sml" (*part.*)
129 (*use "Knowledge/integrate.sml" part. was complete 2009-2
131 (*use "Knowledge/eqsystem.sml" 2002*)
132 use "Knowledge/test.sml" (*new 2011*)
133 use "Knowledge/polyminus.sml" (*part.*)
134 (*use "Knowledge/vect.sml" 2002*)
135 (*use "Knowledge/diffapp.sml" 2002*)
136 (*use "Knowledge/biegelinie.sml" 2002*)
137 (*use "Knowledge/algein.sml" 2002*)
138 use "Knowledge/diophanteq.sml" (*complete*)
139 use "Knowledge/isac.sml" (*part.*)
140 ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}
141 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
142 ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*}
143 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
147 (*=== inhibit exn ?=============================================================
148 ===== inhibit exn ?===========================================================*)
150 (*========== inhibit exn 110503 ================================================
152 "########### testcode inserted vvv ###########################################";
153 "########### testcode inserted ^^^ ###########################################";
155 ============ inhibit exn 110503 ==============================================*)
157 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
158 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)