1.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy	Tue Aug 31 11:10:30 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Tue Aug 31 15:36:57 2010 +0200
     1.3 @@ -297,11 +297,11 @@
     1.4  
     1.5  	       Calc ("op *", eval_binop "#mult_"),
     1.6  
     1.7 -	       Thm ("real_mult_0",num_str real_mult_0),    
     1.8 +	       Thm ("mult_zero_left",num_str @{thm mult_zero_left}),    
     1.9  	       (*"0 * z = 0"*)
    1.10 -	       Thm ("real_mult_1",num_str real_mult_1),     
    1.11 +	       Thm ("mult_1_left",num_str @{thm mult_1_left}),     
    1.12  	       (*"1 * z = z"*)
    1.13 -	       Thm ("real_add_zero_left",num_str real_add_zero_left),
    1.14 +	       Thm ("add_0_left",num_str @{thm add_0_left}),
    1.15  	       (*"0 + z = z"*)
    1.16  	       Thm ("null_minus",num_str null_minus),
    1.17  	       (*"0 - a = -a"*)
    1.18 @@ -328,9 +328,9 @@
    1.19  val klammern_ausmultiplizieren = 
    1.20    Rls{id = "klammern_ausmultiplizieren", preconds = [], 
    1.21        rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls, 
    1.22 -      rules = [Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
    1.23 +      rules = [Thm ("left_distrib" ,num_str @{thm left_distrib}),
    1.24  	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
    1.25 -	       Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
    1.26 +	       Thm ("left_distrib2",num_str @{thm left_distrib}2),
    1.27  	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
    1.28  	       
    1.29  	       Thm ("klammer_mult_minus",num_str klammer_mult_minus),