# HG changeset patch
# User paulson
# Date 935571868 -7200
# Node ID dace49c16aca9fc33a0d4f3ac0add864339339f2
# Parent  59bc887290dfefe1bf01130d015ac788513d6f05
arguably clearer definition of the inductive case of
leads-to.
No proofs had to be changed...

diff -r 59bc887290df -r dace49c16aca src/HOL/UNITY/WFair.thy
--- a/src/HOL/UNITY/WFair.thy	Wed Aug 25 11:02:37 1999 +0200
+++ b/src/HOL/UNITY/WFair.thy	Wed Aug 25 11:04:28 1999 +0200
@@ -39,7 +39,7 @@
     (*Encoding using powerset of the desired axiom
        (!!A. A : S ==> (A,B) : leads F) ==> (Union S, B) : leads F
     *)
-    Union  "(UN A:S. {(A,B)}) : Pow (leads F) ==> (Union S, B) : leads F"
+    Union  "{(A,B) | A. A: S} : Pow (leads F) ==> (Union S, B) : leads F"
 
   monos Pow_mono