1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Tue May 19 12:33:35 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Wed May 20 12:52:09 2020 +0200
     1.3 @@ -133,7 +133,7 @@
     1.4            crls = LinEq_crls, errpats = [], nrls = norm_Poly},
     1.5          @{thm refl})]
     1.6  \<close>
     1.7 -    (* ansprechen mit ["LinEq","solve_univar_equation"] *)
     1.8 +    (* ansprechen mit ["LinEq", "solve_univar_equation"] *)
     1.9  
    1.10  partial_function (tailrec) solve_linear_equation :: "bool \<Rightarrow> real \<Rightarrow> bool list"
    1.11    where
    1.12 @@ -152,7 +152,7 @@
    1.13      Or_to_List e_e)"
    1.14  setup \<open>KEStore_Elems.add_mets
    1.15      [Method.prep_input thy "met_eq_lin" [] Method.id_empty
    1.16 -      (["LinEq","solve_lineq_equation"],
    1.17 +      (["LinEq", "solve_lineq_equation"],
    1.18          [("#Given", ["equality e_e", "solveFor v_v"]),
    1.19            ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e)  has_degree_in v_v) = 1"]),
    1.20            ("#Find",  ["solutions v_v'i'"])],
    1.21 @@ -160,7 +160,7 @@
    1.22            crls = LinEq_crls, errpats = [], nrls = norm_Poly},
    1.23          @{thm solve_linear_equation.simps})]
    1.24  \<close>
    1.25 -ML \<open>Method.from_store' @{theory} ["LinEq","solve_lineq_equation"];\<close>
    1.26 +ML \<open>Method.from_store' @{theory} ["LinEq", "solve_lineq_equation"];\<close>
    1.27  
    1.28  end
    1.29