1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Fri May 07 13:23:24 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Fri May 07 18:12:51 2021 +0200
     1.3 @@ -31,9 +31,9 @@
     1.4  	      Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
     1.5  	      Rule.Eval ("Prog_Expr.lhs"    , Prog_Expr.eval_lhs ""),
     1.6  	      Rule.Eval ("Prog_Expr.rhs"    , Prog_Expr.eval_rhs ""),
     1.7 -	      Rule.Eval ("Poly.has'_degree'_in", eval_has_degree_in ""),
     1.8 - 	      Rule.Eval ("Poly.is'_polyrat'_in", eval_is_polyrat_in ""),
     1.9 -	      Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),    
    1.10 +	      Rule.Eval ("Poly.has_degree_in", eval_has_degree_in ""),
    1.11 + 	      Rule.Eval ("Poly.is_polyrat_in", eval_is_polyrat_in ""),
    1.12 +	      Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),    
    1.13  	      Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
    1.14  	      Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
    1.15  	      Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
    1.16 @@ -160,7 +160,11 @@
    1.17            crls = LinEq_crls, errpats = [], nrls = norm_Poly},
    1.18          @{thm solve_linear_equation.simps})]
    1.19  \<close>
    1.20 -ML \<open>MethodC.from_store' @{theory} ["LinEq", "solve_lineq_equation"];\<close>
    1.21 +ML \<open>
    1.22 +  MethodC.from_store' @{theory} ["LinEq", "solve_lineq_equation"];
    1.23 +\<close> ML \<open>
    1.24 +\<close> ML \<open>
    1.25 +\<close>
    1.26  
    1.27  end
    1.28