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/Cardinal.thy
changeset 81125 ec121999a9cb
parent 76217 8655344f1cf6 
--- a/src/ZF/Cardinal.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/Cardinal.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -25,8 +25,8 @@
     "A \<prec> B \<equiv> A \<lesssim> B \<and> \<not>(A \<approx> B)"
 
 definition
-  cardinal :: "i\<Rightarrow>i"           (\<open>|_|\<close>)  where
-    "|A| \<equiv> (\<mu> i. i \<approx> A)"
+  cardinal :: "i\<Rightarrow>i"  (\<open>(\<open>open_block notation=\<open>mixfix cardinal\<close>\<close>|_|)\<close>)
+  where "|A| \<equiv> (\<mu> i. i \<approx> A)"
 
 definition
   Finite   :: "i\<Rightarrow>o"  where
isabelle