1.1 --- a/src/Tools/isac/Knowledge/RatEq.thy	Sun Sep 22 17:28:55 2013 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy	Sun Sep 22 18:09:05 2013 +0200
     1.3 @@ -117,7 +117,9 @@
     1.4  ruleset' := overwritelthy @{theory} (!ruleset',
     1.5  			[("rateq_erls",rateq_erls)(*FIXXXME:del with rls.rls'*)
     1.6  			 ]);
     1.7 -
     1.8 +*}
     1.9 +setup {* KEStore_Elems.add_rlss [("rateq_erls", (Context.theory_name @{theory}, rateq_erls))] *}
    1.10 +ML {*
    1.11  
    1.12  val RatEq_crls = 
    1.13      remove_rls "RatEq_crls"                                   (*WN: ein Hack*)
    1.14 @@ -149,6 +151,10 @@
    1.15  ruleset' := overwritelthy @{theory} (!ruleset',
    1.16  			[("RatEq_eliminate",RatEq_eliminate)
    1.17  			 ]);
    1.18 +*}
    1.19 +setup {* KEStore_Elems.add_rlss [("RatEq_eliminate",
    1.20 +  (Context.theory_name @{theory}, RatEq_eliminate))] *}
    1.21 +ML {*
    1.22  
    1.23  val RatEq_simplify = prep_rls(
    1.24    Rls {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI", termlessI),
    1.25 @@ -176,6 +182,10 @@
    1.26  ruleset' := overwritelthy @{theory} (!ruleset',
    1.27  			[("RatEq_simplify",RatEq_simplify)
    1.28  			 ]);
    1.29 +*}
    1.30 +setup {* KEStore_Elems.add_rlss [("RatEq_simplify",
    1.31 +  (Context.theory_name @{theory}, RatEq_simplify))] *}
    1.32 +ML {*
    1.33  
    1.34  (*-------------------------Problem-----------------------*)
    1.35  (*