1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Mon Apr 19 20:44:18 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Tue Apr 20 16:58:44 2021 +0200
     1.3 @@ -370,8 +370,8 @@
     1.4  \<close>
     1.5  subsection \<open>Transform an equality into a function\<close>
     1.6  
     1.7 -        (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
     1.8 -               0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
     1.9 +        (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x \<up> 2) (M_b L = 0) -->
    1.10 +               0 = c_2 + c * L + -1 * q_0 / 2 * L \<up> 2*)
    1.11  partial_function (tailrec) function_to_equality :: "bool \<Rightarrow> bool \<Rightarrow> bool"
    1.12    where
    1.13  "function_to_equality fu_n su_b = (
    1.14 @@ -379,7 +379,7 @@
    1.15      fu_n = Take fu_n;
    1.16      bd_v = argument_in (lhs fu_n);
    1.17      va_l = argument_in (lhs su_b);
    1.18 -    eq_u = Substitute [bd_v = va_l] fu_n; \<comment> \<open>([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2\<close>
    1.19 +    eq_u = Substitute [bd_v = va_l] fu_n; \<comment> \<open>([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L \<up> 2\<close>
    1.20      eq_u = Substitute [su_b] eq_u
    1.21    in
    1.22      (Rewrite_Set ''norm_Rational'') eq_u)"
    1.23 @@ -393,8 +393,8 @@
    1.24  				      [Rule.Eval("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
    1.25  				        Rule.Eval("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in")], 
    1.26  				  prls=Rule_Set.empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.empty},
    1.27 -        (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
    1.28 -               0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
    1.29 +        (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x \<up> 2) (M_b L = 0) -->
    1.30 +               0 = c_2 + c * L + -1 * q_0 / 2 * L \<up> 2*)
    1.31          @{thm function_to_equality.simps})]
    1.32  \<close>
    1.33  ML \<open>