# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1283957127 -7200
# Node ID 24609758d219575e92d2307c0ad934c50498c6ef
# Parent  468809a52c9f8ee01b262affd2e702f3fad74bc9
tuned

diff -r 468809a52c9f -r 24609758d219 src/Tools/isac/Knowledge/PolyEq.thy
--- a/src/Tools/isac/Knowledge/PolyEq.thy	Wed Sep 08 16:28:24 2010 +0200
+++ b/src/Tools/isac/Knowledge/PolyEq.thy	Wed Sep 08 16:45:27 2010 +0200
@@ -1463,7 +1463,7 @@
 		(*"?bdv / ?b = (1 / ?b) * ?bdv"*)
 		Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n}),
 		(*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
-		Thm ("nadd_divide_distrib", 
+		Thm ("add_divide_distrib", 
 		     num_str @{thm add_divide_distrib})
 		(*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
 		      WN051031 DOES NOT BELONG TO HERE*)