1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Wed Apr 15 10:07:43 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Wed Apr 15 11:11:54 2020 +0200
     1.3 @@ -174,17 +174,17 @@
     1.4        rew_ord = ("ord_simplify_System",
     1.5  		 ord_simplify_System false @{theory "Integrate"}),
     1.6        erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
     1.7 -      rules = [Rule.Thm ("mult_commute",ThmC.numerals_to_Free @{thm mult.commute}),
     1.8 +      rules = [Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
     1.9  	       (* z * w = w * z *)
    1.10  	       Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
    1.11  	       (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
    1.12 -	       Rule.Thm ("mult_assoc",ThmC.numerals_to_Free @{thm mult.assoc}),		
    1.13 +	       Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),		
    1.14  	       (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
    1.15 -	       Rule.Thm ("add_commute",ThmC.numerals_to_Free @{thm add.commute}),	
    1.16 +	       Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),	
    1.17  	       (*z + w = w + z*)
    1.18 -	       Rule.Thm ("add_left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
    1.19 +	       Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
    1.20  	       (*x + (y + z) = y + (x + z)*)
    1.21 -	       Rule.Thm ("add_assoc",ThmC.numerals_to_Free @{thm add.assoc})	               
    1.22 +	       Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc})	               
    1.23  	       (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
    1.24  	       ], 
    1.25        scr = Rule.EmptyScr};
    1.26 @@ -253,7 +253,7 @@
    1.27  	       (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
    1.28  	       Rule.Rls_ norm_Rational_noadd_fractions(**2**),
    1.29  	       Rule.Rls_ (*order_add_mult_in*) norm_System_noadd_fractions (**1**),
    1.30 -	       Rule.Thm ("sym_mult_assoc",
    1.31 +	       Rule.Thm ("sym_mult.assoc",
    1.32                       ThmC.numerals_to_Free (@{thm mult.assoc} RS @{thm sym}))
    1.33  	       (*Rule.Rls_ discard_parentheses *3**),
    1.34  	       Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
    1.35 @@ -282,7 +282,7 @@
    1.36  (*
    1.37  val simplify_System = 
    1.38      Rule_Set.append_rules "simplify_System" simplify_System_parenthesized
    1.39 -	       [Rule.Thm ("sym_add_assoc",
    1.40 +	       [Rule.Thm ("sym_add.assoc",
    1.41                        ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym}))];
    1.42  *)
    1.43  \<close>