1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Thu Jun 10 12:23:57 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Thu Jun 10 12:48:50 2021 +0200
     1.3 @@ -23,8 +23,6 @@
     1.4    lin_isolate_div:   "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)"
     1.5  
     1.6  ML \<open>
     1.7 -val thy = @{theory};
     1.8 -
     1.9  val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
    1.10    Rule_Set.append_rules "LinEq_prls" Rule_Set.empty 
    1.11  	     [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),