Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
arguably clearer definition of the inductive case of
authorpaulson
Wed, 25 Aug 1999 11:04:28 +0200
changeset 7346 dace49c16aca
parent 7345 59bc887290df
child 7347 ad0ce67e4eb6
arguably clearer definition of the inductive case of leads-to. No proofs had to be changed...
src/HOL/UNITY/WFair.thy file | annotate | diff | comparison | revisions 
--- 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