1 (* Title: tests for xmlsrc/thy-hierarchy.sml |
1 (* Title: "xmlsrc/thy-hierarchy.sml" |
|
2 tests for xmlsrc/thy-hierarchy.sml |
2 Authors: Walther Neuper 060113 |
3 Authors: Walther Neuper 060113 |
3 (c) due to copyright terms |
4 (c) due to copyright terms |
4 |
5 |
5 theory Test_Some imports Isac.Build_Thydata begin |
6 theory Test_Some imports Isac.Build_Thydata begin |
6 ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml" |
7 ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml" |
27 "-----------------------------------------------------------------"; |
28 "-----------------------------------------------------------------"; |
28 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy"; |
29 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy"; |
29 "----------- ..CONTINUED: we adapt some required MINIfunctions ---"; |
30 "----------- ..CONTINUED: we adapt some required MINIfunctions ---"; |
30 "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------"; |
31 "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------"; |
31 "----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---"; |
32 "----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---"; |
32 "-------- fun thms_of --------------------------------------------------------"; |
|
33 "-----------------------------------------------------------------"; |
33 "-----------------------------------------------------------------"; |
34 "-----------------------------------------------------------------"; |
34 "-----------------------------------------------------------------"; |
35 "-----------------------------------------------------------------"; |
35 "-----------------------------------------------------------------"; |
36 |
36 |
37 |
37 |
50 val thy = @{theory Biegelinie}; |
50 val thy = @{theory Biegelinie}; |
51 val thms = thms_of thy; |
51 val thms = thms_of thy; |
52 if map thmID_of_derivation_name' thms = |
52 if map thmID_of_derivation_name' thms = |
53 ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", "Querkraft_Moment", |
53 ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", "Querkraft_Moment", |
54 "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"] then () |
54 "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"] then () |
55 else error "fun thms_of ...changed" |
55 else error "fun thms_of ...changed"; |
|
56 |
|
57 val without_partial_functions = thms_of @{theory Biegelinie}; |
|
58 if length without_partial_functions = 7 then () else error "thms_of Biegelinie changed"; |
56 |
59 |
57 "----------- ### thes2file ... Exception- Match raised -----------"; |
60 "----------- ### thes2file ... Exception- Match raised -----------"; |
58 "----------- ### thes2file ... Exception- Match raised -----------"; |
61 "----------- ### thes2file ... Exception- Match raised -----------"; |
59 "----------- ### thes2file ... Exception- Match raised -----------"; |
62 "----------- ### thes2file ... Exception- Match raised -----------"; |
60 writeln "what to do when you get, e.g. \n\ |
63 writeln "what to do when you get, e.g. \n\ |
265 " <STRING> e_rls </STRING>\n" ^ |
268 " <STRING> e_rls </STRING>\n" ^ |
266 " <GUH> thy_isac_Poly-rls-e_rls </GUH>\n" ^ |
269 " <GUH> thy_isac_Poly-rls-e_rls </GUH>\n" ^ |
267 " </SRLS>\n" ^ |
270 " </SRLS>\n" ^ |
268 " <SCRIPT>\n" ^ |
271 " <SCRIPT>\n" ^ |
269 " <MATHML>\n" ^ |
272 " <MATHML>\n" ^ |
270 " <ISA> Script Stepwise t_t =\n" ^ |
273 " <ISA> auto_generated t_t =\nRepeat\n" ^ |
271 " Repeat\n" ^ |
274 " ((Try (Repeat (Rewrite ''distrib_right'' False)) @@\n" ^ |
272 " ((Try (Repeat (Rewrite ''distrib_right'' False)) @@\n" ^ |
275 " Try (Repeat (Rewrite ''distrib_left'' False)))\n" ^ |
273 " Try (Repeat (Rewrite ''distrib_left'' False)))\n" ^ |
276 " ??.empty) </ISA>\n" ^ |
274 " ??.empty) </ISA>\n" ^ |
|
275 " </MATHML>\n" ^ |
277 " </MATHML>\n" ^ |
276 " </SCRIPT>\n" ^ |
278 " </SCRIPT>\n" ^ |
277 " </RULESET>\n" ^ |
279 " </RULESET>\n" ^ |
278 " <EXPLANATIONS> </EXPLANATIONS>\n" ^ |
280 " <EXPLANATIONS> </EXPLANATIONS>\n" ^ |
279 " <MATHAUTHORS>\n" ^ |
281 " <MATHAUTHORS>\n" ^ |
280 " <STRING> isac-team </STRING>\n" ^ |
282 " <STRING> isac-team </STRING>\n" ^ |
281 " </MATHAUTHORS>\n" ^ |
283 " </MATHAUTHORS>\n" ^ |
282 " <COURSEDESIGNS>\n </COURSEDESIGNS>\n" ^ |
284 " <COURSEDESIGNS>\n" ^ |
|
285 " </COURSEDESIGNS>\n" ^ |
283 "</RULESETDATA>\n") then () |
286 "</RULESETDATA>\n") then () |
284 else error "thydata2xml for rls changed" |
287 else error "thydata2xml for rls changed"; |
285 |
288 |
286 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy"; |
289 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy"; |
287 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy"; |
290 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy"; |
288 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy"; |
291 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy"; |
289 val isacrlsthms = KEStore_Elems.get_rlss @{theory Test_Build_Thydata} |
292 val isacrlsthms = KEStore_Elems.get_rlss @{theory Test_Build_Thydata} |
425 " </MATHAUTHORS>\n" ^ |
428 " </MATHAUTHORS>\n" ^ |
426 " <COURSEDESIGNS>\n" ^ |
429 " <COURSEDESIGNS>\n" ^ |
427 " </COURSEDESIGNS>\n" ^ |
430 " </COURSEDESIGNS>\n" ^ |
428 "</THEOREMDATA>\n") then () else error "thy_isac_Test_Build_Thydata-thm-thm111.xml changed" |
431 "</THEOREMDATA>\n") then () else error "thy_isac_Test_Build_Thydata-thm-thm111.xml changed" |
429 |
432 |
430 "-------- fun thms_of --------------------------------------------------------"; |
|
431 "-------- fun thms_of --------------------------------------------------------"; |
|
432 "-------- fun thms_of --------------------------------------------------------"; |
|
433 val without_partial_functions = thms_of @{theory Biegelinie}; |
|
434 if length without_partial_functions = 7 then () else error "thms_of Biegelinie changed"; |
|