src/HOL/Trancl.thy

--- a/src/HOL/Trancl.thy	Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/Trancl.thy	Fri Oct 02 14:28:39 1998 +0200
@@ -17,7 +17,7 @@
 
 constdefs
   rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [1000] 999)
-  "r^*  ==  lfp(%s. id Un (r O s))"
+  "r^*  ==  lfp(%s. Id Un (r O s))"
 
   trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [1000] 999)
   "r^+  ==  r O rtrancl(r)"
@@ -26,6 +26,6 @@
   reflcl  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [1000] 999)
 
 translations
-  "r^=" == "r Un id"
+  "r^=" == "r Un Id"
 
 end