1.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml	Thu May 30 12:39:13 2019 +0200
     1.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml	Sat Jun 01 11:09:19 2019 +0200
     1.3 @@ -1,4 +1,5 @@
     1.4 -(* Title: tests for xmlsrc/thy-hierarchy.sml
     1.5 +(* Title: "xmlsrc/thy-hierarchy.sml"
     1.6 +     tests for xmlsrc/thy-hierarchy.sml
     1.7     Authors: Walther Neuper 060113
     1.8     (c) due to copyright terms
     1.9  
    1.10 @@ -29,7 +30,6 @@
    1.11  "----------- ..CONTINUED: we adapt some required MINIfunctions ---";
    1.12  "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
    1.13  "----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";
    1.14 -"-------- fun thms_of --------------------------------------------------------";
    1.15  "-----------------------------------------------------------------";
    1.16  "-----------------------------------------------------------------";
    1.17  "-----------------------------------------------------------------";
    1.18 @@ -52,7 +52,10 @@
    1.19  if map thmID_of_derivation_name' thms = 
    1.20    ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", "Querkraft_Moment", 
    1.21     "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"] then ()
    1.22 -else error "fun thms_of ...changed"
    1.23 +else error "fun thms_of ...changed";
    1.24 +
    1.25 +val without_partial_functions = thms_of @{theory Biegelinie};
    1.26 +if length without_partial_functions = 7 then () else error "thms_of Biegelinie changed";
    1.27  
    1.28  "----------- ### thes2file ... Exception- Match raised -----------";
    1.29  "----------- ### thes2file ... Exception- Match raised -----------";
    1.30 @@ -267,11 +270,10 @@
    1.31  "    </SRLS>\n" ^
    1.32  "    <SCRIPT>\n" ^
    1.33  "      <MATHML>\n" ^
    1.34 -"        <ISA> Script Stepwise t_t   =\n" ^
    1.35 -" Repeat\n" ^
    1.36 -"  ((Try (Repeat (Rewrite ''distrib_right'' False)) @@\n" ^
    1.37 -"    Try (Repeat (Rewrite ''distrib_left'' False)))\n" ^
    1.38 -"    ??.empty) </ISA>\n" ^
    1.39 +"        <ISA> auto_generated t_t =\nRepeat\n" ^
    1.40 +" ((Try (Repeat (Rewrite ''distrib_right'' False)) @@\n" ^
    1.41 +"   Try (Repeat (Rewrite ''distrib_left'' False)))\n" ^
    1.42 +"   ??.empty) </ISA>\n" ^
    1.43  "      </MATHML>\n" ^
    1.44  "    </SCRIPT>\n" ^
    1.45  "  </RULESET>\n" ^
    1.46 @@ -279,9 +281,10 @@
    1.47  "  <MATHAUTHORS>\n" ^
    1.48  "    <STRING> isac-team </STRING>\n" ^
    1.49  "  </MATHAUTHORS>\n" ^
    1.50 -"  <COURSEDESIGNS>\n  </COURSEDESIGNS>\n" ^
    1.51 +"  <COURSEDESIGNS>\n" ^
    1.52 +"  </COURSEDESIGNS>\n" ^
    1.53  "</RULESETDATA>\n") then ()
    1.54 -else error "thydata2xml for rls changed"
    1.55 +else error "thydata2xml for rls changed";
    1.56  
    1.57  "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
    1.58  "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
    1.59 @@ -427,8 +430,3 @@
    1.60  "  </COURSEDESIGNS>\n" ^
    1.61  "</THEOREMDATA>\n") then () else error "thy_isac_Test_Build_Thydata-thm-thm111.xml changed"
    1.62  
    1.63 -"-------- fun thms_of --------------------------------------------------------";
    1.64 -"-------- fun thms_of --------------------------------------------------------";
    1.65 -"-------- fun thms_of --------------------------------------------------------";
    1.66 -val without_partial_functions = thms_of @{theory Biegelinie};
    1.67 -if length without_partial_functions = 7 then () else error "thms_of Biegelinie changed";