(* Title: "BridgeLibisabelle/thy-hierarchy.sml"

   Authors: Walther Neuper 060113

   (c) due to copyright terms

theory Test_Some imports Isac.Build_Thydata begin 

ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"

ML_file "xmlsrc/thy-hierarchy.sml"

CAUTION with testing *2file functions -- they are actually writing to ~/tmp

*)

val thy = @{theory "Isac_Knowledge"};

"-----------------------------------------------------------------";

"table of contents -----------------------------------------------";

"-----------------------------------------------------------------";

"----------- fun thms_of -----------------------------------------";

"----------- ### thes2file ... Exception- Match raised -----------";

"----------- search for data error in thes2file ------------------";

"----------- thes2file: thy_containing_rls : rls '...' not in ! --";

"----------- fun Thm.make_thm ------------------------------------";

"----------- correct theIDs for Rule_Set.empty -------------------";

"----------- fun revert_sym_rule --------------------------------------";

"----------- fun thms_of_rlss ------------------------------------";

"----------- repair thydata2xml for rls --------------------------";

"-----------------------------------------------------------------";

"----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";

"----------- ..CONTINUED: we adapt some required MINIfunctions ---";

"----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";

"----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

"----------- fun thms_of -----------------------------------------";

"----------- fun thms_of -----------------------------------------";

"----------- fun thms_of -----------------------------------------";

(*WN160112 WE REPLACED vvv BY "fun thms_of" in src/../thy-hierarchy.sml

val ths = MutabelleExtra.thms_of false @{theory Biegelinie};

(*val it = 

  ["Q' ?x = - qq ?x", "- qq ?x = Q' ?x", "\<not> ?a =!= 0 \<Longrightarrow> (?a * ?f ?x = ?b) = (?f ?x = 1 / ?a * ?b)",

   "Q ?x = M_b' ?x", "M_b' ?x = Q ?x", "y'' ?x = - M_b ?x / EI", "M_b ?x = - EI * y'' ?x"]*)

map ThmC.id_of_thm (thms_of thy) = 

  ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", 

   "Querkraft_Moment", "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"]

*)

val thy = @{theory Biegelinie};

val thms = thms_of thy;

if map ThmC.id_of_thm thms = 

  ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", "Querkraft_Moment", 

   "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"] then ()

else error "fun thms_of ...changed";

val without_partial_functions = thms_of @{theory Biegelinie};

if length without_partial_functions = 7 then () else error "thms_of Biegelinie changed";

"----------- ### thes2file ... Exception- Match raised -----------";

"----------- ### thes2file ... Exception- Match raised -----------";

"----------- ### thes2file ... Exception- Match raised -----------";

writeln "what to do when you get, e.g. \n\

\### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\"]\n\

\### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"integration_rules\"]\n\

\### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"add_new_c\"]\n\

\Exception- Match raised\n";

;

val theID = ["IsacKnowledge","Integrate","Rulesets","add_new_c"];

val thydata = get_the theID;

;

(* HERE WE DO NOT create a file ...

thydata2file "/tmp/" [] theID thydata (*reports Exception- Match in question*);

*)

;

thydata2xml (theID, thydata) (*reported Exception- Match in question*);

val i = 2;

;

val (theID: Thy_Html.theID, Thy_Html.Hrls {guh, coursedesign, mathauthors, thy_rls}) = (theID, thydata);

rls2xml i thy_rls            (*reported Exception- Match in question*);

;

val (j, (thyID, Rule_Set.Sequence data)) = (i, thy_rls);

rls2xml j (thyID, Rule_Set.Sequence data)  (*reported Exception- Match in question*);

;

val (j, (thyID, Rule_Set.Sequence {id, preconds, rew_ord=(ord,_), erls, errpatts, srls, calc, rules, scr})) = 

  (j, (thyID, Rule_Set.Sequence data));

;

rules2xml (j+2*i) thyID rules  (*reports Exception- Match in question*);

(*TODO: Eval + Cal1 in datatypes.sml *)

"----------- search for data error in thes2file ------------------";

"----------- search for data error in thes2file ------------------";

"----------- search for data error in thes2file ------------------";

val TESTdump = Unsynchronized.ref 

  ("path": filepath, ["ids"]: Thy_Html.theID, []: pos, thydata2file, Store.Node ("xxx", [], []): Thy_Html.thydata Store.node);

fun TESTthenode (pa:filepath) ids po wfn (Store.Node (id, [n], ns)) TESTids = 

    let val po' = lev_on po

    in 

      if (ids@[id]) = TESTids

      then

        (TESTdump := (pa, ids, po', wfn, (Store.Node (id, [n], ns))); 

          error "stopped before error, created TESTdump") (* this exn creates right signature*)

      else

        wfn pa po' (ids @ [id]) n; TESTthenodes pa (ids @ [id]) ((lev_dn po'): pos) wfn ns TESTids

    end

and TESTthenodes _ _ _ _ [] _ = ()

  | TESTthenodes pa ids po wfn (n::ns) TESTids =

      (TESTthenode pa ids po wfn n TESTids; TESTthenodes pa ids (lev_on po) wfn ns TESTids);

(* /--- side effects from previous test files ---\*)

    val i = indentation;

    val j = indentation;

(* \--- side effects from previous test files ---/*)

"~~~~~ fun thes2file, args:"; val (p : filepath) = ("/tmp/");

(* recursively descend into thehier just before the error

   by setting TESTids according to the last line in ouput 

   ### thes2file: id = : *)

(TESTthenodes p [] [0] thydata2file (get_thes ()) 

  ["IsacKnowledge","Rational","Rulesets","norm_Rational_parenthesized"] 

handle _(* "stopped before error, created TESTdump" *) => ());

;

(* /----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----\*)

val (pa, ids, po', wfn, (Store.Node (id, [n], ns))) = ! TESTdump; 

;

"~~~~~ fun thydata2file, args:"; val ((xmldata:filepath), (pos:pos), (theID:Thy_Html.theID), thydata) =

  (pa, po', (ids@[id]), n);

"~~~~~ fun thydata2xml, args:"; val (theID, Thy_Html.Hrls {guh, coursedesign, mathauthors, thy_rls}) =

  (theID:Thy_Html.theID, thydata);

"~~~~~ fun rls2xml, args:"; val (j, (thyID, Rule_Set.Sequence data)) = (i, thy_rls);

"~~~~~ fun rls2xm, args:"; val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,

		      srls, calc, errpatts, rules, scr})) = (j, (thyID, "Rule_Set.Sequence", data));

"~~~~~ fun rules2xml, args:"; val (j, thyID, (r::rs)) = ((j+2*i), thyID, rules);

"~~~~~ fun rule2xml, args:"; val (j, thyID, (Rls_ rls)) = (j, thyID, r);

val rls' = (#id o Rule_Set.rep) rls;

(* \----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----/

  another way to tackle this kind of error is shown in

"----------- thes2file: thy_containing_rls : rls '...' not in ! --";   ------------------------*)

"----------- thes2file: thy_containing_rls : rls '...' not in ! --";

"----------- thes2file: thy_containing_rls : rls '...' not in ! --";

"----------- thes2file: thy_containing_rls : rls '...' not in ! --";

val theID = ["IsacKnowledge","Rational","Rulesets","norm_Rational_parenthesized"]

val thydata = get_the theID

;

thydata2xml (theID, thydata);

"----------- fun ThmC_Def.make_thm ------------------------------------";

"----------- fun ThmC_Def.make_thm ------------------------------------";

"----------- fun ThmC_Def.make_thm ------------------------------------";

"~~~~~ fun ThmC_Def.make_thm, args:"; val (thy, part, (thmID : ThmC.id, thm), (mathauthors : Thy_Html.authors)) =

  (@{theory "Biegelinie"}, "IsacKnowledge",

    ("Belastung_Querkraft", Thm.prop_of @{thm Belastung_Querkraft}),

	      ["Walther Neuper 2005 supported by a grant from NMI Austria"]);

    val guh = Thy_Html.thm2guh (part, Context.theory_name thy) thmID

    val theID = guh2theID guh;

if guh = "thy_isac_Biegelinie-thm-Belastung_Querkraft" andalso

  theID = ["IsacKnowledge", "Biegelinie", "Theorems", "Belastung_Querkraft"]

then () else error "store_thm: guh | theID changed";

"----------- correct theIDs for Rule_Set.empty ----------------------------";

"----------- correct theIDs for Rule_Set.empty ----------------------------";

"----------- correct theIDs for Rule_Set.empty ----------------------------";

if thy_containing_rls "Build_Thydata" "empty" = ("IsacScripts", "Know_Store") then ()

else error "thy_containing_rls Rule_Set.empty changed";

show_thes ();

(*shows different assignment for "empty"...

  : 

                                                ["IsacScripts", "Know_Store", "Rulesets", "empty"], 

  :*)

"----------- fun revert_sym_rule --------------------------------------";

"----------- fun revert_sym_rule --------------------------------------";

"----------- fun revert_sym_rule --------------------------------------";

val thy = @{theory Isac_Knowledge}

val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy

  (Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})))

;

if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "-1 * ?z = - ?z"

then () else error "fun revert_sym_rule changed 1";

val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy

  (Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}))

;

if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + -1 * ?b"

then () else error "fun revert_sym_rule changed 2"

"----------- fun thms_of_rlss ------------------------------------";

"----------- fun thms_of_rlss ------------------------------------";

"----------- fun thms_of_rlss ------------------------------------";

val rlss = 

  [("empty" : Rule_Set.id, ("Know_Store": ThyC.id, Rule_Set.empty)),

  ("discard_minus" : Rule_Set.id, ("Poly": ThyC.id, discard_minus))]

;

val [_, (thmID, term)] = thms_of_rlss thy rlss;

(*

if thmID = "real_mult_minus1" (* WAS "??.unknown" *)

then () else error "thms_of_rlss changed"

*)

;

"~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac_Knowledge}, rlss);

val rlss' = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)

  |> map (thms_of_rls o #2 o #2)

    (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"), 

      Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]]*)

  |> flat

    (* = [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"), 

      Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]*)

  |> map (ThmC.revert_sym_rule thy)

    (* = [Thm ("Poly.real_diff_minus", "?a - ?b = ?a + -1 * ?b"), 

      Thm ("Delete.real_mult_minus1", "-1 * ?z = - ?z")] : rule list*)

  |> map (fn Thm (thmID, thm) => (thmID, Thm.prop_of thm))

    (* = [("Poly.real_diff_minus", Const ("HOL.Trueprop", "bool \<Rightarrow> prop") $ ...,

      ("Delete.real_mult_minus1", Const ("HOL.Trueprop", ...)] : (string * term) list*)

  |> gen_distinct (fn ((thmID1, thm1), (thmID2, thm2)) => thmID1 = thmID2);

"----------- repair thydata2xml for rls --------------------------";

"----------- repair thydata2xml for rls --------------------------";

"----------- repair thydata2xml for rls --------------------------";

val theID = ["IsacKnowledge", "Poly", "Rulesets", "expand"]

val hrls = get_the theID

;

if thydata2xml (theID, hrls) = (

"<RULESETDATA>\n" ^

"  <GUH> thy_isac_Poly-rls-expand </GUH>\n" ^

"  <STRINGLIST>\n" ^

"    <STRING> IsacKnowledge </STRING>\n" ^

"    <STRING> Poly </STRING>\n" ^

"    <STRING> Rulesets </STRING>\n" ^

"    <STRING> expand </STRING>\n" ^

"  </STRINGLIST>\n  <RULESET>\n" ^

"    <ID> expand </ID>\n" ^

"    <TYPE> Rls </TYPE>\n" ^

"    <RULES>\n" ^

"      <RULE>\n" ^

"        <TAG> Theorem </TAG>\n" ^

"        <STRING> distrib_right </STRING>\n" ^

"        <GUH> thy_isac_distrib_right-thm-distrib_right </GUH>\n" ^

"      </RULE>\n" ^

"      <RULE>\n" ^

"        <TAG> Theorem </TAG>\n" ^

"        <STRING> distrib_left </STRING>\n" ^

"        <GUH> thy_isac_distrib_left-thm-distrib_left </GUH>\n" ^

"      </RULE>\n" ^

"    </RULES>\n" ^

"    <PRECONDS>" ^

"     </PRECONDS>\n" ^

"    <ORDER>\n" ^

"      <STRING> dummy_ord </STRING>\n" ^

"    </ORDER>\n" ^

"    <ERLS>\n" ^

"      <TAG> Ruleset </TAG>\n" ^

"      <STRING> empty </STRING>\n" ^

"      <GUH> thy_isac_Poly-rls-empty </GUH>\n" ^

"    </ERLS>\n" ^

"    <SRLS>\n" ^

"      <TAG> Ruleset </TAG>\n" ^

"      <STRING> empty </STRING>\n" ^

"      <GUH> thy_isac_Poly-rls-empty </GUH>\n" ^

"    </SRLS>\n" ^

"    <SCRIPT>  </SCRIPT>\n" ^

(*

"    <SCRIPT>\n" ^

"      <MATHML>\n" ^

"        <ISA> auto_generated t_t =\nRepeat\n ((Try (Repeat (Rewrite ''distrib_right'')) #&gt;\n   Try (Repeat (Rewrite ''distrib_left'')))\n   ??.empty) </ISA>\n" ^

"      </MATHML>\n" ^

"    </SCRIPT>\n" ^

*)

"  </RULESET>\n" ^

"  <EXPLANATIONS> </EXPLANATIONS>\n" ^

"  <MATHAUTHORS>\n" ^

"    <STRING> isac-team </STRING>\n" ^

"  </MATHAUTHORS>\n" ^

"  <COURSEDESIGNS>\n" ^

"  </COURSEDESIGNS>\n" ^

"</RULESETDATA>\n") then ()

else error "thydata2xml for rls changed";

"----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";

"----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";

"----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";

  val isacrlsthms = KEStore_Elems.get_rlss @{theory Test_Build_Thydata}

(*                         CHANGE FOR CODE ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)

    |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "prog_expr" (*unpleasant in test*)

    |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "e_rrls"   (*unpleasant in test*)

    |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "empty"    (*unpleasant in test*)

    |> thms_of_rlss @{theory}            (*length =  4*)

  val rlsthmsNOTisac = isacrlsthms       (*length =  2*)

    |> filter (fn (deriv, _) => 

      member op= (map Context.theory_name isabthys') (ThyC.cut_id deriv))

;

val (knowthys', progthys') = ([@{theory Test_Build_Thydata}], [@{theory Test_Build_Thydata}])

;

val thydata_list = 

  collect_part       "IsacKnowledge" knowledge_parent knowthys' @

  (map (collect_isab "Isabelle") rlsthmsNOTisac) @

  collect_part       "IsacScripts" proglang_parent progthys' (* only the thms, no rls *)

;

case thydata_list of                     (*length =  8*)

  [(["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm111"],

    Thy_Html.Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm111", 

    mathauthors = ["isac-team"], thm = _}),

  (["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm222"],

    Thy_Html.Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm222", 

    mathauthors = ["isac-team"], thm = _}),

  (["IsacKnowledge", "Test_Build_Thydata", "Rulesets", "rls111"],

    Thy_Html.Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls111", 

    mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rule_Set.Repeat _)}),

  (["IsacKnowledge", "Test_Build_Thydata", "Rulesets", "rls222"],

    Thy_Html.Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls222", 

    mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rule_Set.Repeat _)}),

  (["Isabelle", "HOL", "Theorems", "refl"],

    Thy_Html.Hthm {coursedesign = [], fillpats = [], guh = "thy_isab_HOL-thm-refl", 

    mathauthors = ["Isabelle team, TU Munich"], thm = _}),

  (["Isabelle", "Fun", "Theorems", "o_def"], Thy_Html.Hthm {coursedesign = [], fillpats = [], 

    guh = "thy_isab_Fun-thm-o_def", mathauthors = ["Isabelle team, TU Munich"], thm = _}),

  (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm111"],

    Thy_Html.Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm111", 

    mathauthors = ["isac-team"], thm = _}),

  (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm222"],

    Thy_Html.Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm222", 

    mathauthors = ["isac-team"], thm = _})] => ()

| _ => error "collect thydata from Test_Build_Thydata changed";

;

(* we store locally on MINIthehier instead on Know_Store, see Know_Store: *)

    fun add_the (thydata, theID) = Thy_Html.add_thydata ([], theID) thydata;

val thes = map (fn (a, b) => (b, a)) thydata_list

val MINIthehier = (fold add_the thes) (KEStore_Elems.get_thes @{theory Test_Build_Thydata});

"----------- ..CONTINUED: we adapt some required MINIfunctions ---";

"----------- ..CONTINUED: we adapt some required MINIfunctions ---";

"----------- ..CONTINUED: we adapt some required MINIfunctions ---";

fun MINIget_the (theID : Thy_Html.theID) = Store.get MINIthehier theID theID (*see ptyps.sml*)

fun MINIthy_hierarchy2file (path:filepath) = 

  str2file (path ^ "thy_hierarchy.xml") 

    ("<NODE>\n" ^

    "  <ID> theory hierarchy </ID>\n" ^

    "  <NO> 1 </NO>\n" ^

    "  <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^

    (hierarchy_guh MINIthehier) ^

    "</NODE>");

fun MINIthes2file (p : filepath) = thenodes p [] [0] thydata2file MINIthehier;

"----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";

"----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";

"----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";

case MINIget_the ["IsacScripts", "Test_Build_Thydata", "Theorems", "thm111"] of

  Thy_Html.Hthm {guh = "thy_scri_Test_Build_Thydata-thm-thm111", ...} => ()

| _ => error "MINIget_the thm111 changed"

;

val path = "/tmp/"

;

MINIthy_hierarchy2file path            (* ---> /tmp/thy_hierarchy.xml *);

writeln (file2str path "thy_hierarchy.xml") (* better check in editor *)

;

MINIthes2file path                               (* ---> /tmp/thy_... *);

"----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";

"----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";

"----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";

"~~~~~ fun MINIthes2file, args:"; val (path) = ("/tmp/");

"~~~~~ and thenodes, args:"; val (pa, ids, po, wfn, (n::ns)) = 

  (path, [], [0], thydata2file, MINIthehier);

"~~~~~ fun thenode, args:"; val ((pa : filepath), ids, po, wfn, (Store.Node (id, [n], ns))) = 

  (pa, ids, po, wfn, n);

val po' = lev_on po;

(*wfn pa po' (ids @ [id]) n  -------------> writes xml to file; we want xml before written: *)

(* we take (theID, thydata) from thydata_list ABOVE: *)

case hd thydata_list of

  (["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm111"],

    Thy_Html.Hthm {guh = "thy_isac_Test_Build_Thydata-thm-thm111", mathauthors = ["isac-team"], ...}) => ()

| _ => error "a change inhibits successful continuation of this test";

val (theID, thydata) = hd thydata_list;

"~~~~~ fun thydata2file, args:"; val ((path : filepath), (pos : pos), (theID : Thy_Html.theID), thydata) =

  (pa, po', (*ids @ [id]*)theID, (*n*)thydata);

"~~~~~ fun thydata2xml, args:"; val ((theID, Thy_Html.Hthm {guh, coursedesign, mathauthors, fillpats, thm}))=

  ((theID, thydata));

"~~~~~ to str2file return val:"; val (xml) = 

      "<THEOREMDATA>\n" ^

      indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^

      id2xml i theID ^

      thm''2xml i thm ^

      indt i ^ "<PROOF>\n" ^

      extref2xml (i+i) "Proof of the theorem" 

	      ("http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/" ^

	        nth 2 theID ^ ".html") ^

	    indt i ^  "</PROOF>\n" ^

	    indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^

	    authors2xml i "MATHAUTHORS" mathauthors ^

	    authors2xml i "COURSEDESIGNS" coursedesign ^

	    "</THEOREMDATA>\n"

;

if xml = ("<THEOREMDATA>\n" ^

"  <GUH> thy_isac_Test_Build_Thydata-thm-thm111 </GUH>\n" ^

"  <STRINGLIST>\n" ^

"    <STRING> IsacKnowledge </STRING>\n" ^

"    <STRING> Test_Build_Thydata </STRING>\n" ^

"    <STRING> Theorems </STRING>\n" ^

"    <STRING> thm111 </STRING>\n" ^

"  </STRINGLIST>\n" ^

"  <THEOREM>\n" ^

"    <ID> thm111 </ID>\n" ^

"    <MATHML>\n" ^

"      <ISA> ?thm111.0 = ?thm111.0 + 111 </ISA>\n" ^

"    </MATHML>\n" ^

"  </THEOREM>\n" ^

"  <PROOF>\n" ^

"    <EXTREF>\n" ^

"      <TEXT> Proof of the theorem </TEXT>\n" ^

"      <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Test_Build_Thydata.html </URL>\n" ^

"    </EXTREF>\n" ^

"  </PROOF>\n" ^

"  <EXPLANATIONS> </EXPLANATIONS>\n" ^

"  <MATHAUTHORS>\n" ^

"    <STRING> isac-team </STRING>\n" ^

"  </MATHAUTHORS>\n" ^

"  <COURSEDESIGNS>\n" ^

"  </COURSEDESIGNS>\n" ^

"</THEOREMDATA>\n") then () else error "thy_isac_Test_Build_Thydata-thm-thm111.xml changed"