1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Wed May 26 16:19:41 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Wed May 26 16:24:05 2021 +0200
     1.3 @@ -393,17 +393,15 @@
     1.4  	 scr = Rule.Empty_Prog};
     1.5  \<close>
     1.6  
     1.7 -setup \<open>KEStore_Elems.add_rlss 
     1.8 -  [("simplify_System_parenthesized",
     1.9 -    (Context.theory_name @{theory}, prep_rls' simplify_System_parenthesized)), 
    1.10 -  ("simplify_System", (Context.theory_name @{theory}, prep_rls' simplify_System)), 
    1.11 -  ("isolate_bdvs", (Context.theory_name @{theory}, prep_rls' isolate_bdvs)), 
    1.12 -  ("isolate_bdvs_4x4", (Context.theory_name @{theory}, prep_rls' isolate_bdvs_4x4)), 
    1.13 -  ("order_system", (Context.theory_name @{theory}, prep_rls' order_system)), 
    1.14 -  ("order_add_mult_System", (Context.theory_name @{theory}, prep_rls' order_add_mult_System)), 
    1.15 -  ("norm_System_noadd_fractions", 
    1.16 -    (Context.theory_name @{theory}, prep_rls' norm_System_noadd_fractions)), 
    1.17 -  ("norm_System", (Context.theory_name @{theory}, prep_rls' norm_System))]\<close>
    1.18 +setup_rule
    1.19 +  simplify_System_parenthesized = \<open>prep_rls' simplify_System_parenthesized\<close> and
    1.20 +  simplify_System = \<open>prep_rls' simplify_System\<close> and
    1.21 +  isolate_bdvs = \<open>prep_rls' isolate_bdvs\<close> and
    1.22 +  isolate_bdvs_4x4 = \<open>prep_rls' isolate_bdvs_4x4\<close> and 
    1.23 +  order_system = \<open>prep_rls' order_system\<close> and 
    1.24 +  order_add_mult_System = \<open>prep_rls' order_add_mult_System\<close> and
    1.25 +  norm_System_noadd_fractions = \<open>prep_rls' norm_System_noadd_fractions\<close> and
    1.26 +  norm_System = \<open>prep_rls' norm_System\<close>
    1.27  
    1.28  
    1.29  section \<open>Problems\<close>