1.1 --- a/src/Tools/isac/Knowledge/Test.thy	Wed Apr 15 10:07:43 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Wed Apr 15 11:11:54 2020 +0200
     1.3 @@ -442,7 +442,7 @@
     1.4        rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), 
     1.5        erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [],
     1.6        rules = 
     1.7 -      [Rule.Thm ("sym_add_assoc",ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym})),
     1.8 +      [Rule.Thm ("sym_add.assoc",ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym})),
     1.9         Rule.Thm ("sym_rmult_assoc",ThmC.numerals_to_Free (@{thm rmult_assoc} RS @{thm sym}))],
    1.10        scr = Rule.EmptyScr
    1.11        };      
    1.12 @@ -453,7 +453,7 @@
    1.13        rules = 
    1.14        [Rule.Thm ("radd_commute",ThmC.numerals_to_Free @{thm radd_commute}),
    1.15         Rule.Thm ("radd_left_commute",ThmC.numerals_to_Free @{thm radd_left_commute}),
    1.16 -       Rule.Thm ("add_assoc",ThmC.numerals_to_Free @{thm add.assoc}),
    1.17 +       Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
    1.18         Rule.Thm ("rmult_commute",ThmC.numerals_to_Free @{thm rmult_commute}),
    1.19         Rule.Thm ("rmult_left_commute",ThmC.numerals_to_Free @{thm rmult_left_commute}),
    1.20         Rule.Thm ("rmult_assoc",ThmC.numerals_to_Free @{thm rmult_assoc})],
    1.21 @@ -486,7 +486,7 @@
    1.22  
    1.23                 Rule.Thm ("radd_commute",ThmC.numerals_to_Free @{thm radd_commute}), 
    1.24  	       Rule.Thm ("radd_left_commute",ThmC.numerals_to_Free @{thm radd_left_commute}),
    1.25 -	       Rule.Thm ("add_assoc",ThmC.numerals_to_Free @{thm add.assoc}),
    1.26 +	       Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
    1.27  	       Rule.Thm ("rmult_commute",ThmC.numerals_to_Free @{thm rmult_commute}),
    1.28  	       Rule.Thm ("rmult_left_commute",ThmC.numerals_to_Free @{thm rmult_left_commute}),
    1.29  	       Rule.Thm ("rmult_assoc",ThmC.numerals_to_Free @{thm rmult_assoc}),
    1.30 @@ -624,17 +624,17 @@
    1.31  	       (*"0 + z = z"*)
    1.32  
    1.33  	       (*AC-rewriting*)
    1.34 -	       Rule.Thm ("mult_commute",ThmC.numerals_to_Free @{thm mult.commute}),
    1.35 +	       Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
    1.36  	       (* z * w = w * z *)
    1.37  	       Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
    1.38  	       (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
    1.39 -	       Rule.Thm ("mult_assoc",ThmC.numerals_to_Free @{thm mult.assoc}),		
    1.40 +	       Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),		
    1.41  	       (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
    1.42 -	       Rule.Thm ("add_commute",ThmC.numerals_to_Free @{thm add.commute}),	
    1.43 +	       Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),	
    1.44  	       (*z + w = w + z*)
    1.45 -	       Rule.Thm ("add_left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
    1.46 +	       Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
    1.47  	       (*x + (y + z) = y + (x + z)*)
    1.48 -	       Rule.Thm ("add_assoc",ThmC.numerals_to_Free @{thm add.assoc}),	               
    1.49 +	       Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),	               
    1.50  	       (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
    1.51  
    1.52  	       Rule.Thm ("sym_realpow_twoI",
    1.53 @@ -725,13 +725,13 @@
    1.54  	Rule.Num_Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
    1.55  	Rule.Num_Calc ("Prog_Expr.pow", (**)eval_binop "#power_"),
    1.56          (*	       
    1.57 -	 Rule.Thm ("mult_commute",ThmC.numerals_to_Free @{thm mult_commute}),		
    1.58 +	 Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),		
    1.59          (*AC-rewriting*)
    1.60  	Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
    1.61 -	Rule.Thm ("mult_assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
    1.62 -	Rule.Thm ("add_commute",ThmC.numerals_to_Free @{thm add_commute}),	
    1.63 -	Rule.Thm ("add_left_commute",ThmC.numerals_to_Free @{thm add_left_commute}),
    1.64 -	Rule.Thm ("add_assoc",ThmC.numerals_to_Free @{thm add_assoc}),
    1.65 +	Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
    1.66 +	Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),	
    1.67 +	Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
    1.68 +	Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
    1.69  	*)
    1.70  	
    1.71  	Rule.Thm ("sym_realpow_twoI",