1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Wed Sep 08 16:28:24 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Wed Sep 08 16:45:27 2010 +0200
     1.3 @@ -1463,7 +1463,7 @@
     1.4  		(*"?bdv / ?b = (1 / ?b) * ?bdv"*)
     1.5  		Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n}),
     1.6  		(*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
     1.7 -		Thm ("nadd_divide_distrib", 
     1.8 +		Thm ("add_divide_distrib", 
     1.9  		     num_str @{thm add_divide_distrib})
    1.10  		(*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
    1.11  		      WN051031 DOES NOT BELONG TO HERE*)