interrupted test/../integrate.sml for calculate.
strange observation: "===== test 4" shows, that thm requires type constraint
in order to be applied;
just done for PolyEq.thy in some axioms "separate_*".
come back to that after repair of calculate.
1 (* Title Run_Tests on isac
2 $ cd /usr/local/isabisac/test/Tools/isac
3 $ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy &
5 RESTART emacs after having created a new Isac heap.
6 was sml/RTEST-root.sml in isac-2002
8 12345678901234567890123456789012345678901234567890123456789012345678901234567890
9 10 20 30 40 50 60 70 80
12 theory Test_Isac imports Isac begin
14 ML{* writeln "**** run the tests **************************************" *};
15 ML {* Toplevel.debug := true; *}
18 (*+ check kbtest/diffapp.sml for additional items in met-model*)
21 (* use"script_if.sml"; WN03 missing: is_rootequation_in*)
25 use"interface-xml.sml";
26 (* use"testdaten.sml"; no update after dropping 'errorBound'*)
29 ML{* writeln "**** run systests complete ******************************" *};
33 use"../../../test/Tools/isac/ProgLang/termC.sml"; (*part.*)
34 use"../../../test/Tools/isac/ProgLang/calculate.sml"; (*part.*)
35 use"../../../test/Tools/isac/ProgLang/rewrite.sml"; (*part.*)
44 use "../../../test/Tools/isac/Interpret/calchead.sml" (*part.*)
48 use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);
55 use"pbl-met-hierarchy.sml";
56 use"thy-hierarchy.sml";
58 cd"smltest/FE-interface";
62 ML{* writeln "**** run tests on math-engine complete ******************" *};
64 cd"smltest/IsacKnowledge";
70 use "../../../test/Tools/isac/Knowledge/integrate.sml"; (*part.*)
73 (*use"inssort.sml"; problems with recdef in Isabelle2002*)
76 use"../../../test/Tools/isac/Knowledge/poly.sml"; (*part.*)
79 use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
80 ? also check others without check 'diff.behav.'*);
82 use"rational.sml" (*TODO add_fractions_p throws overflow-exn WN*);
83 use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln',
84 for simplification search MG
85 erls: 98a(1) 104a(1) 104a(2) 68a *);
99 use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test"
101 *** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library"
102 *** Theory loader: the error(s) above occurred while examining theory "Foo_Language"
104 use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"
106 use_thy "../../../test/Pure/Isar/Test_Parse_Term"
107 use_thy "../../../test/Pure/Isar/Test_Parsers"
109 ML{* writeln "**** run tests on IsacKnowledge complete ****************" *};
111 val path = "/home/neuper/proto3/testsml2xml/";
112 pbl_hierarchy2file (path ^ "pbl/");
113 pbls2file (path ^ "pbl/");
114 met_hierarchy2file (path ^ "met/");
115 mets2file (path ^ "met/");
116 thy_hierarchy2file (path ^ "thy/");
117 thes2file (path ^ "thy/");
120 ML{* writeln "**** tested creation of xmldata *************************" *};
123 writeln "=========================================================";
125 writeln "**** run systests complete ***************** re-organize!";
126 writeln "**** run tests on math-engine complete ******************";
127 writeln "**** run tests on IsacKnowledge complete ****************";
128 writeln "**** build isac kernel + run tests complete *************";
129 writeln "**** tested creation of xmldata *************************";