1.1 --- a/doc-isac/jrocnik/Test_Complex.thy	Sun Oct 09 07:44:22 2022 +0200
     1.2 +++ b/doc-isac/jrocnik/Test_Complex.thy	Sun Oct 09 09:01:29 2022 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  *}
     1.5  ML {*
     1.6  @{term "Complex 1 2 + Complex 3 4"};
     1.7 -print_depth 999; str2term "Complex 1 2 + Complex 3 4"; print_depth 999;
     1.8 +print_depth 999; TermC.parse_test @{context} "Complex 1 2 + Complex 3 4"; print_depth 999;
     1.9  *}
    1.10  ML {*
    1.11  @{term "Complex 1 2 * Complex 3 4"};
    1.12 @@ -25,12 +25,12 @@
    1.13  ML {*
    1.14  val a = @{term "Complex 1 2"};
    1.15  atomty a;
    1.16 -val a = str2term "Complex 1 2";
    1.17 +val a = TermC.parse_test @{context} "Complex 1 2";
    1.18  atomty a;
    1.19  *}
    1.20  ML {*
    1.21  val b = @{term "Complex 3 4"};
    1.22 -val b = str2term "Complex 3 4";
    1.23 +val b = TermC.parse_test @{context} "Complex 3 4";
    1.24  (*a + (b::complex); ERROR: term + term*)
    1.25  *}
    1.26  
    1.27 @@ -45,7 +45,7 @@
    1.28  *}
    1.29  ML {*
    1.30    val thm = @{thm "complex_add"};
    1.31 -  val t = str2term "Complex 1 2 + Complex 3 4";
    1.32 +  val t = TermC.parse_test @{context} "Complex 1 2 + Complex 3 4";
    1.33    val SOME _ = rewrite_ thy ro er true thm t;
    1.34    val SOME (t', _) = rewrite_ thy ro er true thm t;
    1.35    "Complex (1 + 3) (2 + 4)" = term2str t';
    1.36 @@ -66,7 +66,7 @@
    1.37  *}
    1.38  ML {*
    1.39  
    1.40 -val t = str2term "(Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))";
    1.41 +val t = TermC.parse_test @{context} "(Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))";
    1.42  term2str t = "Complex 1 2 * (Complex 3 4 + Complex 5 6)";
    1.43  atomty t;
    1.44  
    1.45 @@ -90,7 +90,7 @@
    1.46  		  ];
    1.47  *}
    1.48  ML {*
    1.49 -val t = str2term "inverse (Complex (2::real) (4::real))";
    1.50 +val t = TermC.parse_test @{context} "inverse (Complex (2::real) (4::real))";
    1.51  term2str t = "inverse Complex (2) (4)";
    1.52  atomty t;
    1.53  *}

     2.1 --- a/doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Sun Oct 09 07:44:22 2022 +0200
     2.2 +++ b/doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex	Sun Oct 09 09:01:29 2022 +0200
     2.3 @@ -1667,7 +1667,7 @@
     2.4  %     ];\end{verbatim}
     2.5  %   \item Define exression:
     2.6  %   \begin{verbatim}
     2.7 -%   val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
     2.8 +%   val sample_term = TermC.parse_test @{context} "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}
     2.9  %   \item Apply ruleset:
    2.10  %   \begin{verbatim}
    2.11  %   val SOME (sample_term', asm) = 

     3.1 --- a/doc-isac/mat-eng-de.tex	Sun Oct 09 07:44:22 2022 +0200
     3.2 +++ b/doc-isac/mat-eng-de.tex	Sun Oct 09 09:01:29 2022 +0200
     3.3 @@ -70,9 +70,9 @@
     3.4     > "a + b * 3";
     3.5        val it = "a + b * 3" : string
     3.6  \end{verbatim}}
     3.7 -\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:
     3.8 +\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:
     3.9  {\footnotesize\begin{verbatim}
    3.10 -   > str2term "a + b * 3";
    3.11 +   > TermC.parse_test @{context} "a + b * 3";
    3.12        val it =
    3.13           Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
    3.14                 Free ("a", "RealDef.real") $
    3.15 @@ -81,7 +81,7 @@
    3.16  \end{verbatim}}
    3.17  \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:
    3.18  {\footnotesize\begin{verbatim}
    3.19 -   > val t = str2term "a + b * 3";
    3.20 +   > val t = TermC.parse_test @{context} "a + b * 3";
    3.21        val t =  
    3.22           Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
    3.23                 Free ("a", "RealDef.real") $
    3.24 @@ -154,7 +154,7 @@
    3.25  
    3.26  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
    3.27  
    3.28 -\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.
    3.29 +\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.
    3.30  {\footnotesize\begin{verbatim}
    3.31     > parse Isac.thy "a + b";
    3.32        val it = Some "a + b" : Thm.cterm Library.option

     4.1 --- a/doc-isac/mat-eng-en.tex	Sun Oct 09 07:44:22 2022 +0200
     4.2 +++ b/doc-isac/mat-eng-en.tex	Sun Oct 09 09:01:29 2022 +0200
     4.3 @@ -33,7 +33,7 @@
     4.4  %"----------- eval_sort -------------------------------------------";
     4.5  %"----------- eval_sort -------------------------------------------";
     4.6  %"----------- eval_sort -------------------------------------------";
     4.7 -%val ts = str2term "[c_2 = 0, -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0]";
     4.8 +%val ts = TermC.parse_test @{context} "[c_2 = 0, -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0]";
     4.9  %val ts' = sort (ord_simplify_Integral_ false (assoc_thy"Isac.thy") [])
    4.10  %              (isalist2list ts);
    4.11  %terms2str ts';
    4.12 @@ -41,7 +41,7 @@
    4.13  %if term2str ts'' = "[-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0, c_2 = 0]"
    4.14  %then () else raise error "eqsystem.sml eval_sort 1";
    4.15  %
    4.16 -%val t = str2term "order_system [c_2 = 0,\
    4.17 +%val t = TermC.parse_test @{context} "order_system [c_2 = 0,\
    4.18  %                \-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0]";
    4.19  %val Some (str,_) = eval_order_system "" "EqSystem.order'_system" t "";
    4.20  %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 ()

     5.1 --- a/doc-isac/mat-eng.sml	Sun Oct 09 07:44:22 2022 +0200
     5.2 +++ b/doc-isac/mat-eng.sml	Sun Oct 09 09:01:29 2022 +0200
     5.3 @@ -3,8 +3,8 @@
     5.4  
     5.5  (*2.2. *)
     5.6  "a + b * 3";
     5.7 -str2term "a + b * 3";
     5.8 -val term = str2term "a + b * 3";
     5.9 +TermC.parse_test @{context} "a + b * 3";
    5.10 +val term = TermC.parse_test @{context} "a + b * 3";
    5.11  atomt term;
    5.12  atomty term;
    5.13  

     6.1 --- a/doc-isac/mlehnfeld/bacc/projektbericht.tex	Sun Oct 09 07:44:22 2022 +0200
     6.2 +++ b/doc-isac/mlehnfeld/bacc/projektbericht.tex	Sun Oct 09 09:01:29 2022 +0200
     6.3 @@ -461,8 +461,8 @@
     6.4  ML {*
     6.5    "artifically inject assumptions";
     6.6    val (SOME (iform, cform), SOME (ires, cres)) = get_obj g_loc pt (fst p);
     6.7 -  val ctxt = insert_assumptions [str2term "x < sub_asm_out",
     6.8 -                                 str2term "a < sub_asm_local"] cres;
     6.9 +  val ctxt = insert_assumptions [TermC.parse_test @{context} "x < sub_asm_out",
    6.10 +                                 TermC.parse_test @{context} "a < sub_asm_local"] cres;
    6.11    val pt = update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt));
    6.12  *}
    6.13  

     7.1 --- a/src/Tools/isac/Build_Isac.thy	Sun Oct 09 07:44:22 2022 +0200
     7.2 +++ b/src/Tools/isac/Build_Isac.thy	Sun Oct 09 09:01:29 2022 +0200
     7.3 @@ -162,6 +162,10 @@
     7.4  (*//-----------------------------------------------------------------------------------------\\*)
     7.5  (*\\-----------------------------------------------------------------------------------------//*)
     7.6  begin
     7.7 +ML \<open>
     7.8 +\<close> ML \<open>
     7.9 +\<close> ML \<open>
    7.10 +\<close> 
    7.11  
    7.12  text \<open>
    7.13    show theory dependencies using the graph browser,