1.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Wed Sep 01 15:19:47 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Wed Sep 01 16:15:13 2010 +0200
     1.3 @@ -935,21 +935,21 @@
     1.4  "(Repeat                                                    " ^
     1.5  "((Try (Repeat (Rewrite real_diff_minus         False))) @@ " ^ 
     1.6  
     1.7 -" (Try (Repeat (Rewrite real_add_mult_distrib   False))) @@ " ^	 
     1.8 -" (Try (Repeat (Rewrite real_add_mult_distrib2  False))) @@ " ^	
     1.9 -" (Try (Repeat (Rewrite real_diff_mult_distrib  False))) @@ " ^	
    1.10 -" (Try (Repeat (Rewrite real_diff_mult_distrib2 False))) @@ " ^	
    1.11 +" (Try (Repeat (Rewrite left_distrib   False))) @@ " ^	 
    1.12 +" (Try (Repeat (Rewrite right_distrib  False))) @@ " ^	
    1.13 +" (Try (Repeat (Rewrite left_diff_distrib  False))) @@ " ^	
    1.14 +" (Try (Repeat (Rewrite right_diff_distrib False))) @@ " ^	
    1.15  
    1.16 -" (Try (Repeat (Rewrite real_mult_1             False))) @@ " ^		   
    1.17 -" (Try (Repeat (Rewrite real_mult_0             False))) @@ " ^		   
    1.18 -" (Try (Repeat (Rewrite real_add_zero_left      False))) @@ " ^	 
    1.19 +" (Try (Repeat (Rewrite mult_1_left             False))) @@ " ^		   
    1.20 +" (Try (Repeat (Rewrite mult_zero_left             False))) @@ " ^		   
    1.21 +" (Try (Repeat (Rewrite add_0_left      False))) @@ " ^	 
    1.22  
    1.23  " (Try (Repeat (Rewrite real_mult_commute       False))) @@ " ^		
    1.24  " (Try (Repeat (Rewrite real_mult_left_commute  False))) @@ " ^	
    1.25  " (Try (Repeat (Rewrite real_mult_assoc         False))) @@ " ^		
    1.26 -" (Try (Repeat (Rewrite real_add_commute        False))) @@ " ^		
    1.27 -" (Try (Repeat (Rewrite real_add_left_commute   False))) @@ " ^	 
    1.28 -" (Try (Repeat (Rewrite real_add_assoc          False))) @@ " ^	 
    1.29 +" (Try (Repeat (Rewrite add_commute        False))) @@ " ^		
    1.30 +" (Try (Repeat (Rewrite add_left_commute   False))) @@ " ^	 
    1.31 +" (Try (Repeat (Rewrite add_assoc          False))) @@ " ^	 
    1.32  
    1.33  " (Try (Repeat (Rewrite sym_realpow_twoI        False))) @@ " ^	 
    1.34  " (Try (Repeat (Rewrite realpow_plus_1          False))) @@ " ^	 
    1.35 @@ -994,9 +994,9 @@
    1.36  " (Try (Repeat (Rewrite real_plus_minus_binom1  False))) @@ " ^
    1.37  " (Try (Repeat (Rewrite real_plus_minus_binom2  False))) @@ " ^
    1.38  
    1.39 -" (Try (Repeat (Rewrite real_mult_1             False))) @@ " ^
    1.40 -" (Try (Repeat (Rewrite real_mult_0             False))) @@ " ^
    1.41 -" (Try (Repeat (Rewrite real_add_zero_left      False))) @@ " ^
    1.42 +" (Try (Repeat (Rewrite mult_1_left             False))) @@ " ^
    1.43 +" (Try (Repeat (Rewrite mult_zero_left             False))) @@ " ^
    1.44 +" (Try (Repeat (Rewrite add_0_left      False))) @@ " ^
    1.45  
    1.46  " (Try (Repeat (Calculate plus  ))) @@ " ^
    1.47  " (Try (Repeat (Calculate times ))) @@ " ^