changeset 5608 | a82a038a3e7a |
parent 3499 | ce1664057431 |
child 6906 | 46652582f831 |
--- 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