--- a/src/HOL/Trancl.thy Wed Mar 06 14:19:39 1996 +0100
+++ b/src/HOL/Trancl.thy Fri Mar 08 13:11:09 1996 +0100
@@ -11,14 +11,18 @@
*)
Trancl = Lfp + Relation +
-consts
- rtrancl :: "('a * 'a)set => ('a * 'a)set" ("(_^*)" [100] 100)
- trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [100] 100)
+
+constdefs
+ rtrancl :: "('a * 'a)set => ('a * 'a)set" ("(_^*)" [100] 100)
+ "r^* == lfp(%s. id Un (r O s))"
+
+ trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [100] 100)
+ "r^+ == r O rtrancl(r)"
+
syntax
- reflcl :: "('a*'a)set => ('a*'a)set" ("(_^=)" [100] 100)
-defs
- rtrancl_def "r^* == lfp(%s. id Un (r O s))"
- trancl_def "r^+ == r O rtrancl(r)"
+ reflcl :: "('a*'a)set => ('a*'a)set" ("(_^=)" [100] 100)
+
translations
- "r^=" == "r Un id"
+ "r^=" == "r Un id"
+
end