src/Tools/isac/Knowledge/LinEq.thy
changeset 52155 e4ddf21390fd
parent 52148 aabc6c8e930a
child 55276 ce872d7781d2
     1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Thu Oct 24 14:08:32 2013 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Thu Oct 24 15:00:44 2013 +0200
     1.3 @@ -70,10 +70,6 @@
     1.4       Calc ("Atools.pow" ,eval_binop "#power_"),
     1.5       *)
     1.6      ];
     1.7 -
     1.8 -ruleset' := overwritelthy @{theory} (!ruleset',
     1.9 -			[("LinEq_erls",LinEq_erls)(*FIXXXME:del with rls.rls'*)
    1.10 -			 ]);
    1.11  *}
    1.12  setup {* KEStore_Elems.add_rlss 
    1.13    [("LinEq_erls", (Context.theory_name @{theory}, LinEq_erls))] *}
    1.14 @@ -97,9 +93,6 @@
    1.15  		Calc ("Atools.pow" ,eval_binop "#power_")
    1.16  		],
    1.17         scr = EmptyScr}:rls);
    1.18 -
    1.19 -ruleset' := overwritelthy @{theory} (!ruleset',
    1.20 -			  [("LinPoly_simplify",LinPoly_simplify)]);
    1.21  *}
    1.22  setup {* KEStore_Elems.add_rlss 
    1.23    [("LinPoly_simplify", (Context.theory_name @{theory}, LinPoly_simplify))] *}
    1.24 @@ -121,8 +114,6 @@
    1.25  	      (*   bx=c -> x=c/b *)  
    1.26  	      ],
    1.27       scr = EmptyScr}:rls);
    1.28 -ruleset' := overwritelthy @{theory} (!ruleset',
    1.29 -			[("LinEq_simplify",LinEq_simplify)]);
    1.30  *}
    1.31  setup {* KEStore_Elems.add_rlss 
    1.32    [("LinEq_simplify", (Context.theory_name @{theory}, LinEq_simplify))] *}