equal
deleted
inserted
replaced
75 cd"smltest/IsacKnowledge"; |
75 cd"smltest/IsacKnowledge"; |
76 use"atools.sml"; |
76 use"atools.sml"; |
77 use"complex.sml"; |
77 use"complex.sml"; |
78 use"diff.sml"; |
78 use"diff.sml"; |
79 use"diffapp.sml"; |
79 use"diffapp.sml"; |
80 (**) |
80 *) |
81 use"Knowledge/integrate.sml"; |
81 ML {*print_depth 99*} |
82 (**) |
82 |
|
83 ML {* |
|
84 fun term2str trm = Print_Mode.setmp (Print_Mode.input :: |
|
85 filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) |
|
86 (Syntax.string_of_term @{context}) trm; |
|
87 val trm = str2term "a+b"; term2str trm; |
|
88 val trm = str2term "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3"; term2str trm; |
|
89 "========================================================="; |
|
90 *} |
|
91 |
|
92 use "Knowledge/integrate.sml"; |
|
93 (* |
83 use"equation.sml"; |
94 use"equation.sml"; |
84 (*use"inssort.sml"; problems with recdef in Isabelle2002*) |
95 (*use"inssort.sml"; problems with recdef in Isabelle2002*) |
85 use"logexp.sml"; |
96 use"logexp.sml"; |
86 use"poly.sml"; |
97 use"poly.sml"; |
87 use"polyminus.sml"; |
98 use"polyminus.sml"; |
102 use"eqsystem.sml"; |
113 use"eqsystem.sml"; |
103 use"biegelinie.sml"; |
114 use"biegelinie.sml"; |
104 use"algein.sml"; |
115 use"algein.sml"; |
105 cd "../.."; |
116 cd "../.."; |
106 *) |
117 *) |
|
118 use_thy "../../Pure/Isar/Test_Parse_Term" |
|
119 use_thy "../../Pure/Isar/Test_Parsers" |
|
120 |
107 ML{* writeln "**** run tests on IsacKnowledge complete ****************" *}; |
121 ML{* writeln "**** run tests on IsacKnowledge complete ****************" *}; |
108 (* |
122 (* |
109 val path = "/home/neuper/proto2/testsml2xml/"; |
123 val path = "/home/neuper/proto2/testsml2xml/"; |
110 pbl_hierarchy2file (path ^ "pbl/"); |
124 pbl_hierarchy2file (path ^ "pbl/"); |
111 pbls2file (path ^ "pbl/"); |
125 pbls2file (path ^ "pbl/"); |