1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Wed May 26 16:19:41 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Wed May 26 16:24:05 2021 +0200
     1.3 @@ -319,17 +319,14 @@
     1.4  
     1.5  val prep_rls' = Auto_Prog.prep_rls @{theory};
     1.6  \<close>
     1.7 -setup \<open>KEStore_Elems.add_rlss 
     1.8 -  [("integration_rules", (Context.theory_name @{theory}, prep_rls' integration_rules)), 
     1.9 -  ("add_new_c", (Context.theory_name @{theory}, prep_rls' add_new_c)), 
    1.10 -  ("simplify_Integral", (Context.theory_name @{theory}, prep_rls' simplify_Integral)), 
    1.11 -  ("integration", (Context.theory_name @{theory}, prep_rls' integration)), 
    1.12 -  ("separate_bdv2", (Context.theory_name @{theory}, prep_rls' separate_bdv2)),
    1.13 -
    1.14 -  ("norm_Rational_noadd_fractions", (Context.theory_name @{theory},
    1.15 -    prep_rls' norm_Rational_noadd_fractions)), 
    1.16 -  ("norm_Rational_rls_noadd_fractions", (Context.theory_name @{theory},
    1.17 -    prep_rls' norm_Rational_rls_noadd_fractions))]\<close>
    1.18 +setup_rule
    1.19 +  integration_rules = \<open>prep_rls' integration_rules\<close> and
    1.20 +  add_new_c = \<open>prep_rls' add_new_c\<close> and
    1.21 +  simplify_Integral = \<open>prep_rls' simplify_Integral\<close> and
    1.22 +  integration = \<open>prep_rls' integration\<close> and
    1.23 +  separate_bdv2 = \<open>prep_rls' separate_bdv2\<close> and
    1.24 +  norm_Rational_noadd_fractions = \<open>prep_rls' norm_Rational_noadd_fractions\<close> and
    1.25 +  norm_Rational_rls_noadd_fractions = \<open>prep_rls' norm_Rational_rls_noadd_fractions\<close>
    1.26  
    1.27  (** problems **)
    1.28  setup \<open>KEStore_Elems.add_pbts