1.1 --- a/src/Tools/isac/Knowledge/Test.thy	Wed Sep 01 16:43:58 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Thu Sep 02 15:11:23 2010 +0200
     1.3 @@ -295,7 +295,7 @@
     1.4        rew_ord = ("e_rew_ord",e_rew_ord), 
     1.5        erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
     1.6        rules = 
     1.7 -      [Thm ("sym_radd_assoc",num_str (@{thm radd_assoc} RS @{thm sym})),
     1.8 +      [Thm ("sym_add_assoc",num_str (@{thm add_assoc} RS @{thm sym})),
     1.9         Thm ("sym_rmult_assoc",num_str (@{thm rmult_assoc} RS @{thm sym}))],
    1.10        scr = Script ((term_of o the o (parse thy)) 
    1.11        "empty_script")
    1.12 @@ -307,7 +307,7 @@
    1.13        rules = 
    1.14        [Thm ("radd_commute",num_str @{thm radd_commute}),
    1.15         Thm ("radd_left_commute",num_str @{thm radd_left_commute}),
    1.16 -       Thm ("radd_assoc",num_str @{thm radd_assoc}),
    1.17 +       Thm ("add_assoc",num_str @{thm add_assoc}),
    1.18         Thm ("rmult_commute",num_str @{thm rmult_commute}),
    1.19         Thm ("rmult_left_commute",num_str @{thm rmult_left_commute}),
    1.20         Thm ("rmult_assoc",num_str @{thm rmult_assoc})],
    1.21 @@ -339,7 +339,7 @@
    1.22  	
    1.23    "     (Try (Repeat (Rewrite radd_commute False))) @@        " ^
    1.24    "     (Try (Repeat (Rewrite radd_left_commute False))) @@   " ^
    1.25 -  "     (Try (Repeat (Rewrite radd_assoc False))) @@          " ^
    1.26 +  "     (Try (Repeat (Rewrite add_assoc False))) @@          " ^
    1.27    "     (Try (Repeat (Rewrite rmult_commute False))) @@       " ^
    1.28    "     (Try (Repeat (Rewrite rmult_left_commute False))) @@  " ^
    1.29    "     (Try (Repeat (Rewrite rmult_assoc False))) @@         " ^
    1.30 @@ -392,7 +392,7 @@
    1.31  
    1.32                 Thm ("radd_commute",num_str @{thm radd_commute}), 
    1.33  	       Thm ("radd_left_commute",num_str @{thm radd_left_commute}),
    1.34 -	       Thm ("radd_assoc",num_str @{thm radd_assoc}),
    1.35 +	       Thm ("add_assoc",num_str @{thm add_assoc}),
    1.36  	       Thm ("rmult_commute",num_str @{thm rmult_commute}),
    1.37  	       Thm ("rmult_left_commute",num_str @{thm rmult_left_commute}),
    1.38  	       Thm ("rmult_assoc",num_str @{thm rmult_assoc}),
    1.39 @@ -1267,7 +1267,7 @@
    1.40  	       (*"a - b = a + (-1) * b"*)
    1.41  	       Thm ("left_distrib" ,num_str @{thm left_distrib}),
    1.42  	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
    1.43 -	       Thm ("left_distrib2",num_str @{thm left_distrib2}),
    1.44 +	       Thm ("right_distrib",num_str @{thm right_distrib}),
    1.45  	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
    1.46  	       Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
    1.47  	       (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
    1.48 @@ -1366,7 +1366,6 @@
    1.49  	      ("TIMES" , ("op *", eval_binop "#mult_")),
    1.50  	      ("POWER", ("Atools.pow", eval_binop "#power_"))
    1.51  	      ],
    1.52 -      (*asm_thm = [],*)
    1.53        rules = [Thm ("real_plus_binom_pow2"  ,num_str @{thm real_plus_binom_pow2}),     
    1.54  	       (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
    1.55  	       Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),    
    1.56 @@ -1398,7 +1397,7 @@
    1.57  
    1.58               (*  Thm ("left_distrib" ,num_str @{thm left_distrib}}),	
    1.59  		(*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
    1.60 -	       Thm ("left_distrib2",num_str @{thm left_distrib}2}),	
    1.61 +	       Thm ("right_distrib",num_str @{thm right_distrib}),	
    1.62  	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
    1.63  	       Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}}),	
    1.64  	       (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)