1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Wed May 26 16:19:41 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Wed May 26 16:24:05 2021 +0200
     1.3 @@ -852,29 +852,29 @@
     1.4      scr = Rule.Empty_Prog});
     1.5  \<close>
     1.6  
     1.7 -setup \<open>KEStore_Elems.add_rlss 
     1.8 -  [("calculate_Rational", (Context.theory_name @{theory}, calculate_Rational)), 
     1.9 -  ("calc_rat_erls", (Context.theory_name @{theory}, calc_rat_erls)), 
    1.10 -  ("rational_erls", (Context.theory_name @{theory}, rational_erls)), 
    1.11 -  ("cancel_p", (Context.theory_name @{theory}, cancel_p)), 
    1.12 -  ("add_fractions_p", (Context.theory_name @{theory}, add_fractions_p)),
    1.13 - 
    1.14 -  ("add_fractions_p_rls", (Context.theory_name @{theory}, add_fractions_p_rls)), 
    1.15 -  ("powers_erls", (Context.theory_name @{theory}, powers_erls)), 
    1.16 -  ("powers", (Context.theory_name @{theory}, powers)), 
    1.17 -  ("rat_mult_divide", (Context.theory_name @{theory}, rat_mult_divide)), 
    1.18 -  ("reduce_0_1_2", (Context.theory_name @{theory}, reduce_0_1_2)),
    1.19 - 
    1.20 -  ("rat_reduce_1", (Context.theory_name @{theory}, rat_reduce_1)), 
    1.21 -  ("norm_rat_erls", (Context.theory_name @{theory}, norm_rat_erls)), 
    1.22 -  ("norm_Rational", (Context.theory_name @{theory}, norm_Rational)), 
    1.23 -  ("norm_Rational_rls", (Context.theory_name @{theory}, norm_Rational_rls)), 
    1.24 -  ("norm_Rational_min", (Context.theory_name @{theory}, norm_Rational_min)),
    1.25 -  ("norm_Rational_parenthesized", (Context.theory_name @{theory}, norm_Rational_parenthesized)),
    1.26 - 
    1.27 -  ("rat_mult_poly", (Context.theory_name @{theory}, rat_mult_poly)), 
    1.28 -  ("rat_mult_div_pow", (Context.theory_name @{theory}, rat_mult_div_pow)), 
    1.29 -  ("cancel_p_rls", (Context.theory_name @{theory}, cancel_p_rls))]\<close>
    1.30 +setup_rule
    1.31 +  calculate_Rational = calculate_Rational and
    1.32 +  calc_rat_erls = calc_rat_erls and
    1.33 +  rational_erls = rational_erls and
    1.34 +  cancel_p = cancel_p and
    1.35 +  add_fractions_p = add_fractions_p and
    1.36 +
    1.37 +  add_fractions_p_rls = add_fractions_p_rls and
    1.38 +  powers_erls = powers_erls and
    1.39 +  powers = powers and
    1.40 +  rat_mult_divide = rat_mult_divide and
    1.41 +  reduce_0_1_2 = reduce_0_1_2 and
    1.42 +
    1.43 +  rat_reduce_1 = rat_reduce_1 and
    1.44 +  norm_rat_erls = norm_rat_erls and
    1.45 +  norm_Rational = norm_Rational and
    1.46 +  norm_Rational_rls = norm_Rational_rls and
    1.47 +  norm_Rational_min = norm_Rational_min and
    1.48 +  norm_Rational_parenthesized = norm_Rational_parenthesized and
    1.49 +
    1.50 +  rat_mult_poly = rat_mult_poly and
    1.51 +  rat_mult_div_pow = rat_mult_div_pow and
    1.52 +  cancel_p_rls = cancel_p_rls
    1.53  
    1.54  section \<open>A problem for simplification of rationals\<close>
    1.55  setup \<open>KEStore_Elems.add_pbts