"--------- encode \<up> -> ^ ---------------------------------------";

 "--------- encode < -> &lt and > -> &gt --------------------------";

 "--------- fun rm_doublets '-4 * b \<up>\<up>\<up> 2 / (...' -----------";

 "--------- fun decode '-4 * b \<up>\<up>\<up> 2 / (...' ----------------";

 "--------- encode \<up> -> ^ ---------------------------------------";

 "--------- encode \<up> -> ^ ---------------------------------------";

 "--------- encode \<up> -> ^ ---------------------------------------";

 val str = "a\<up>2+b\<up>2=c\<up>2";

 if decode str = "a\<up>2+b\<up>2=c\<up>2" then ()

 else error "mathml.sml: diff.behav. in encode \<up> -> ^";

 "--------- encode < -> &lt; and > -> &gt; --------------------------";

 "--------- encode < -> &lt; and > -> &gt; --------------------------";

 "--------- encode < -> &lt; and > -> &gt; --------------------------";

 val str = "?bdv occurs_in ?b; 0 < ?n |] ==> ?a / ?b  \<up>  ?n = ?a * ?b  \<up>  - ?n";

 if decode str = "?bdv occurs_in ?b; 0 &lt; ?n |] ==&gt; ?a / ?b  \<up>  ?n = ?a * ?b  \<up>  - ?n" then ()

 else error "mathml.sml: diff.behav. in encode '<' and '>'";

 (*========== inhibit exn AK110725 ================================================

 "----- check 'manually' the xml-output of calling functions ------";

 formula2xml 1 (TermC.str2term str);

 (* AK110725 

 (*TermC.str2term str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b  \<up>  ?n = ?a * ?b  \<up>  - ?n"

                    Failed to TermC.parse term*)*)

 "~~~~~ fun TermC.str2term, args:"; val (str) = (str);

 ThyC.get_theory "Isac_Knowledge";

 TermC.parse_patt;

 TermC.parse_patt (ThyC.get_theory "Isac_Knowledge");

 (*TermC.parse_patt (ThyC.get_theory "Isac_Knowledge") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b  \<up>  ?n = ?a * ?b  \<up>  - ?n"

 Failed to TermC.parse term*)*)

 "~~~~~ fun TermC.parse_patt, args:"; val (thy, str) = ((ThyC.get_theory "Isac_Knowledge"), str);

 (thy, str) 

 |>> ThyC.to_ctxt

 (*|-> Proof_Context.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b  \<up>  ?n = ?a * ?b  \<up>  - ?n"

 Failed to TermC.parse term*)*)

 Proof_Context.read_term_pattern;

 (@{theory "Isac_Knowledge"}, str) |>> ThyC.to_ctxt;

 "~~~~~ fun Proof_Context.read_term_pattern, args:"; val () = ();

 (*AK110725 To be continued...*)

 *)

 (*==================================================================*)

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

 "exported from struct --------------------------------------------";

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

 ========== inhibit exn AK110725 ================================================*)