| changeset 3842 | b55686a7b22c |
| parent 3413 | c1f63cc3a768 |
| child 3947 | eb707467f8c5 |
--- a/src/HOL/WF.thy Fri Oct 10 18:37:49 1997 +0200 +++ b/src/HOL/WF.thy Fri Oct 10 19:02:28 1997 +0200 @@ -10,7 +10,7 @@ constdefs wf :: "('a * 'a)set => bool" - "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))" + "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))" acyclic :: "('a*'a)set => bool" "acyclic r == !x. (x,x) ~: r^+"