1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Sun Sep 22 17:28:55 2013 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Sun Sep 22 18:09:05 2013 +0200
     1.3 @@ -74,6 +74,10 @@
     1.4  ruleset' := overwritelthy @{theory} (!ruleset',
     1.5  			[("LinEq_erls",LinEq_erls)(*FIXXXME:del with rls.rls'*)
     1.6  			 ]);
     1.7 +*}
     1.8 +setup {* KEStore_Elems.add_rlss 
     1.9 +  [("LinEq_erls", (Context.theory_name @{theory}, LinEq_erls))] *}
    1.10 +ML {*
    1.11      
    1.12  val LinPoly_simplify = prep_rls(
    1.13    Rls {id = "LinPoly_simplify", preconds = [], 
    1.14 @@ -96,6 +100,10 @@
    1.15  
    1.16  ruleset' := overwritelthy @{theory} (!ruleset',
    1.17  			  [("LinPoly_simplify",LinPoly_simplify)]);
    1.18 +*}
    1.19 +setup {* KEStore_Elems.add_rlss 
    1.20 +  [("LinPoly_simplify", (Context.theory_name @{theory}, LinPoly_simplify))] *}
    1.21 +ML {*
    1.22  
    1.23  (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
    1.24  val LinEq_simplify = prep_rls(
    1.25 @@ -115,6 +123,10 @@
    1.26       scr = EmptyScr}:rls);
    1.27  ruleset' := overwritelthy @{theory} (!ruleset',
    1.28  			[("LinEq_simplify",LinEq_simplify)]);
    1.29 +*}
    1.30 +setup {* KEStore_Elems.add_rlss 
    1.31 +  [("LinEq_simplify", (Context.theory_name @{theory}, LinEq_simplify))] *}
    1.32 +ML {*
    1.33  
    1.34  (*----------------------------- problem types --------------------------------*)
    1.35  (*