updated "op +", "op -", "op *". "HOL.divide" in src & test
find . -type f -exec sed -i s/"\"op +\""/"\"Groups.plus_class.plus\""/g {} \;
find . -type f -exec sed -i s/"\"op -\""/"\"Groups.minus_class.minus\""/g {} \;
find . -type f -exec sed -i s/"\"op *\""/"\"Groups.times_class.times\""/g {} \;
find . -type f -exec sed -i s/"\"HOL.divide\""/"\"Rings.inverse_class.divide\""/g {} \;
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 ******************************" *};
32 use"calculate-float.sml";
47 type_of @{term "[x_1+1=2,x_2=0]"};
49 @{term "solveForVars"};
50 type_of @{term "[x_1,x_2]::real list"};
53 type_of @{term "ss''' :: bool list"};
55 use "Interpret/calchead.sml" (*part.*)
59 use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);
66 use"pbl-met-hierarchy.sml";
67 use"thy-hierarchy.sml";
69 cd"smltest/FE-interface";
73 ML{* writeln "**** run tests on math-engine complete ******************" *};
75 cd"smltest/IsacKnowledge";
90 use "Knowledge/integrate.sml";
93 (*use"inssort.sml"; problems with recdef in Isabelle2002*)
97 use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
98 ? also check others without check 'diff.behav.'*);
100 use"rational.sml" (*TODO add_fractions_p throws overflow-exn WN*);
101 use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln',
102 for simplification search MG
103 erls: 98a(1) 104a(1) 104a(2) 68a *);
116 use_thy "../../Pure/Isar/Test_Parse_Term"
117 use_thy "../../Pure/Isar/Test_Parsers"
119 ML{* writeln "**** run tests on IsacKnowledge complete ****************" *};
121 val path = "/home/neuper/proto2/testsml2xml/";
122 pbl_hierarchy2file (path ^ "pbl/");
123 pbls2file (path ^ "pbl/");
124 met_hierarchy2file (path ^ "met/");
125 mets2file (path ^ "met/");
126 thy_hierarchy2file (path ^ "thy/");
127 thes2file (path ^ "thy/");
130 ML{* writeln "**** tested creation of xmldata *************************" *};
133 writeln "=========================================================";
135 writeln "**** run systests complete ***************** re-organize!";
136 writeln "**** run tests on math-engine complete ******************";
137 writeln "**** run tests on IsacKnowledge complete ****************";
138 writeln "**** build isac kernel + run tests complete *************";
139 writeln "**** tested creation of xmldata *************************";