# HG changeset patch
# User wneuper <Walther.Neuper@jku.at>
# Date 1665298889 -7200
# Node ID 04f8699d2c9d219317ecb6e3e63ddc8beaaca225
# Parent  f92963a33fe383c042bf4c537a8ac7a90343f49b
eliminate term2str in doc-isac

diff -r f92963a33fe3 -r 04f8699d2c9d doc-isac/jrocnik/Test_Complex.thy
--- a/doc-isac/jrocnik/Test_Complex.thy	Sun Oct 09 07:44:22 2022 +0200
+++ b/doc-isac/jrocnik/Test_Complex.thy	Sun Oct 09 09:01:29 2022 +0200
@@ -6,7 +6,7 @@
 *}
 ML {*
 @{term "Complex 1 2 + Complex 3 4"};
-print_depth 999; str2term "Complex 1 2 + Complex 3 4"; print_depth 999;
+print_depth 999; TermC.parse_test @{context} "Complex 1 2 + Complex 3 4"; print_depth 999;
 *}
 ML {*
 @{term "Complex 1 2 * Complex 3 4"};
@@ -25,12 +25,12 @@
 ML {*
 val a = @{term "Complex 1 2"};
 atomty a;
-val a = str2term "Complex 1 2";
+val a = TermC.parse_test @{context} "Complex 1 2";
 atomty a;
 *}
 ML {*
 val b = @{term "Complex 3 4"};
-val b = str2term "Complex 3 4";
+val b = TermC.parse_test @{context} "Complex 3 4";
 (*a + (b::complex); ERROR: term + term*)
 *}
 
@@ -45,7 +45,7 @@
 *}
 ML {*
   val thm = @{thm "complex_add"};
-  val t = str2term "Complex 1 2 + Complex 3 4";
+  val t = TermC.parse_test @{context} "Complex 1 2 + Complex 3 4";
   val SOME _ = rewrite_ thy ro er true thm t;
   val SOME (t', _) = rewrite_ thy ro er true thm t;
   "Complex (1 + 3) (2 + 4)" = term2str t';
@@ -66,7 +66,7 @@
 *}
 ML {*
 
-val t = str2term "(Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))";
+val t = TermC.parse_test @{context} "(Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))";
 term2str t = "Complex 1 2 * (Complex 3 4 + Complex 5 6)";
 atomty t;
 
@@ -90,7 +90,7 @@
 		  ];
 *}
 ML {*
-val t = str2term "inverse (Complex (2::real) (4::real))";
+val t = TermC.parse_test @{context} "inverse (Complex (2::real) (4::real))";
 term2str t = "inverse Complex (2) (4)";
 atomty t;
 *}
diff -r f92963a33fe3 -r 04f8699d2c9d doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex
--- a/doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Sun Oct 09 07:44:22 2022 +0200
+++ b/doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Sun Oct 09 09:01:29 2022 +0200
@@ -1667,7 +1667,7 @@
 %     ];\end{verbatim}
 %   \item Define exression:
 %   \begin{verbatim}
-%   val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
+%   val sample_term = TermC.parse_test @{context} "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
 %   \item Apply ruleset:
 %   \begin{verbatim}
 %   val SOME (sample_term', asm) = 
diff -r f92963a33fe3 -r 04f8699d2c9d doc-isac/mat-eng-de.tex
--- a/doc-isac/mat-eng-de.tex	Sun Oct 09 07:44:22 2022 +0200
+++ b/doc-isac/mat-eng-de.tex	Sun Oct 09 09:01:29 2022 +0200
@@ -70,9 +70,9 @@
    > "a + b * 3";
       val it = "a + b * 3" : string
 \end{verbatim}}
-\noindent ``a + b * 3'' ist also ein string (eine Zeichenfolge). In dieser Form weiss der Computer nicht, dass z.B. eine Multiplikation {\em vor} einer Addition zu rechnen ist. Isabelle braucht dazu eine andere Darstellung f\"ur Formeln. In diese kann man mit der Funktion {\tt str2term} (string to term) umrechnen:
+\noindent ``a + b * 3'' ist also ein string (eine Zeichenfolge). In dieser Form weiss der Computer nicht, dass z.B. eine Multiplikation {\em vor} einer Addition zu rechnen ist. Isabelle braucht dazu eine andere Darstellung f\"ur Formeln. In diese kann man mit der Funktion {\tt TermC.parse_test @{context}} (string to term) umrechnen:
 {\footnotesize\begin{verbatim}
-   > str2term "a + b * 3";
+   > TermC.parse_test @{context} "a + b * 3";
       val it =
          Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
                Free ("a", "RealDef.real") $
@@ -81,7 +81,7 @@
 \end{verbatim}}
 \noindent Diese Form heisst {\tt term} und ist nicht f\"ur den Menschen zum lesen gedacht. Isabelle braucht sie aber intern zum Rechnen. Wir wollen sie mit Hilfe von {\tt val} (value) auf der Variable {\tt t} speichern:
 {\footnotesize\begin{verbatim}
-   > val t = str2term "a + b * 3";
+   > val t = TermC.parse_test @{context} "a + b * 3";
       val t =  
          Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
                Free ("a", "RealDef.real") $
@@ -154,7 +154,7 @@
 
 Wollen Sie wissen, wie die einzelnen Rechengesetze aussehen, k\"onnen Sie im Internet folgenden Link ansehen: http://isabelle.in.tum.de/dist/library/HOL/Groups.html
 
-\paragraph{} Der Vorgang, bei dem aus einem {\tt string} ein Term entsteht, nennt man Parsing. Dazu wird Wissen aus der Theorie ben\"otigt, denn {\tt str2term} nimmt intern eine parse-Funktion, bei der immer das gesamte \isac{}-Wissen verwendet wird. Bei dieser Funktion wird weiters festgelegt, aus welcher Theorie das Wissen genommen werden soll.
+\paragraph{} Der Vorgang, bei dem aus einem {\tt string} ein Term entsteht, nennt man Parsing. Dazu wird Wissen aus der Theorie ben\"otigt, denn {\tt TermC.parse_test @{context}} nimmt intern eine parse-Funktion, bei der immer das gesamte \isac{}-Wissen verwendet wird. Bei dieser Funktion wird weiters festgelegt, aus welcher Theorie das Wissen genommen werden soll.
 {\footnotesize\begin{verbatim}
    > parse Isac.thy "a + b";
       val it = Some "a + b" : Thm.cterm Library.option
diff -r f92963a33fe3 -r 04f8699d2c9d doc-isac/mat-eng-en.tex
--- a/doc-isac/mat-eng-en.tex	Sun Oct 09 07:44:22 2022 +0200
+++ b/doc-isac/mat-eng-en.tex	Sun Oct 09 09:01:29 2022 +0200
@@ -33,7 +33,7 @@
 %"----------- eval_sort -------------------------------------------";
 %"----------- eval_sort -------------------------------------------";
 %"----------- eval_sort -------------------------------------------";
-%val ts = str2term "[c_2 = 0, -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0]";
+%val ts = TermC.parse_test @{context} "[c_2 = 0, -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0]";
 %val ts' = sort (ord_simplify_Integral_ false (assoc_thy"Isac.thy") [])
 %              (isalist2list ts);
 %terms2str ts';
@@ -41,7 +41,7 @@
 %if term2str ts'' = "[-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0, c_2 = 0]"
 %then () else raise error "eqsystem.sml eval_sort 1";
 %
-%val t = str2term "order_system [c_2 = 0,\
+%val t = TermC.parse_test @{context} "order_system [c_2 = 0,\
 %                \-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0]";
 %val Some (str,_) = eval_order_system "" "EqSystem.order'_system" t "";
 %if str = "order_system [c_2 = 0, -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0] = [-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0, c_2 = 0]" then ()
diff -r f92963a33fe3 -r 04f8699d2c9d doc-isac/mat-eng.sml
--- a/doc-isac/mat-eng.sml	Sun Oct 09 07:44:22 2022 +0200
+++ b/doc-isac/mat-eng.sml	Sun Oct 09 09:01:29 2022 +0200
@@ -3,8 +3,8 @@
 
 (*2.2. *)
 "a + b * 3";
-str2term "a + b * 3";
-val term = str2term "a + b * 3";
+TermC.parse_test @{context} "a + b * 3";
+val term = TermC.parse_test @{context} "a + b * 3";
 atomt term;
 atomty term;
 
diff -r f92963a33fe3 -r 04f8699d2c9d doc-isac/mlehnfeld/bacc/projektbericht.tex
--- a/doc-isac/mlehnfeld/bacc/projektbericht.tex	Sun Oct 09 07:44:22 2022 +0200
+++ b/doc-isac/mlehnfeld/bacc/projektbericht.tex	Sun Oct 09 09:01:29 2022 +0200
@@ -461,8 +461,8 @@
 ML {*
   "artifically inject assumptions";
   val (SOME (iform, cform), SOME (ires, cres)) = get_obj g_loc pt (fst p);
-  val ctxt = insert_assumptions [str2term "x < sub_asm_out",
-                                 str2term "a < sub_asm_local"] cres;
+  val ctxt = insert_assumptions [TermC.parse_test @{context} "x < sub_asm_out",
+                                 TermC.parse_test @{context} "a < sub_asm_local"] cres;
   val pt = update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt));
 *}
 
diff -r f92963a33fe3 -r 04f8699d2c9d src/Tools/isac/Build_Isac.thy
--- a/src/Tools/isac/Build_Isac.thy	Sun Oct 09 07:44:22 2022 +0200
+++ b/src/Tools/isac/Build_Isac.thy	Sun Oct 09 09:01:29 2022 +0200
@@ -162,6 +162,10 @@
 (*//-----------------------------------------------------------------------------------------\\*)
 (*\\-----------------------------------------------------------------------------------------//*)
 begin
+ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> 
 
 text \<open>
   show theory dependencies using the graph browser,