1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Tue Aug 31 11:10:30 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Tue Aug 31 15:36:57 2010 +0200
     1.3 @@ -1349,11 +1349,11 @@
     1.4  	       (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
     1.5  	       Thm ("real_mult_assoc",num_str real_mult_assoc),		
     1.6  	       (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
     1.7 -	       Thm ("real_add_commute",num_str real_add_commute),	
     1.8 +	       Thm ("add_commute",num_str @{thm add_commute}),	
     1.9  	       (*z + w = w + z*)
    1.10 -	       Thm ("real_add_left_commute",num_str real_add_left_commute),
    1.11 +	       Thm ("add_left_commute",num_str @{thm add_left_commute}),
    1.12  	       (*x + (y + z) = y + (x + z)*)
    1.13 -	       Thm ("real_add_assoc",num_str real_add_assoc)	               
    1.14 +	       Thm ("add_assoc",num_str @{thm add_assoc})	               
    1.15  	       (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
    1.16  	       ], scr = EmptyScr}:rls);
    1.17  
    1.18 @@ -1418,8 +1418,8 @@
    1.19  		(*"?bdv / ?b = (1 / ?b) * ?bdv"*)
    1.20  		Thm ("separate_1_bdv_n", num_str separate_1_bdv_n),
    1.21  		(*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
    1.22 -		Thm ("real_add_divide_distrib", 
    1.23 -		     num_str real_add_divide_distrib)
    1.24 +		Thm ("nadd_divide_distrib", 
    1.25 +		     num_str @{thm nadd_divide_distrib})
    1.26  		(*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
    1.27  		      WN051031 DOES NOT BELONG TO HERE*)
    1.28  		];