1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Mon Jul 30 16:41:08 2012 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Tue Jul 31 15:16:47 2012 +0200
     1.3 @@ -80,8 +80,7 @@
     1.4         rew_ord = ("termlessI",termlessI), 
     1.5         erls = LinEq_erls, 
     1.6         srls = Erls, 
     1.7 -       calc = [], 
     1.8 -       (*asm_thm = [],*)
     1.9 +       calc = [], errpatts = [],
    1.10         rules = [
    1.11  		Thm  ("real_assoc_1",num_str @{thm real_assoc_1}),
    1.12  		Calc ("Groups.plus_class.plus",eval_binop "#add_"),
    1.13 @@ -104,8 +103,7 @@
    1.14       rew_ord = ("e_rew_ord",e_rew_ord),
    1.15       erls = LinEq_erls,
    1.16       srls = Erls,
    1.17 -     calc = [],
    1.18 -     (*asm_thm = [("lin_isolate_div","")],*)
    1.19 +     calc = [], errpatts = [],
    1.20       rules = [
    1.21  	      Thm("lin_isolate_add1",num_str @{thm lin_isolate_add1}), 
    1.22  	      (* a+bx=0 -> bx=-a *)