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/ZF/Constructible/L_axioms.thy
changeset 61393 8673ec68c798
parent 60770 240563fbf41d
child 61798 27f3c10b0b50 
--- a/src/ZF/Constructible/L_axioms.thy	Sat Oct 10 22:02:23 2015 +0200
+++ b/src/ZF/Constructible/L_axioms.thy	Sat Oct 10 22:08:43 2015 +0200
@@ -131,7 +131,7 @@
       terms become enormous!\<close>
 definition
   L_Reflects :: "[i=>o,[i,i]=>o] => prop"  ("(3REFLECTS/ [_,/ _])") where
-    "REFLECTS[P,Q] == (??Cl. Closed_Unbounded(Cl) &
+    "REFLECTS[P,Q] == (\<Or>Cl. Closed_Unbounded(Cl) &
                            (\<forall>a. Cl(a) \<longrightarrow> (\<forall>x \<in> Lset(a). P(x) \<longleftrightarrow> Q(a,x))))"
isabelle