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))] *}