Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/UNITY/WFair.thy
changeset 7346 dace49c16aca
parent 6801 9e0037839d63
child 8006 299127ded09d 
--- 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
isabelle