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/OrdQuant.thy
changeset 81125 ec121999a9cb
parent 80917 2a77bc3b4eac 
--- a/src/ZF/OrdQuant.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/OrdQuant.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -330,7 +330,7 @@
 subsubsection\<open>Sets as Classes\<close>
 
 definition
-  setclass :: "[i,i] \<Rightarrow> o"       (\<open>##_\<close> [40] 40)  where
+  setclass :: "[i,i] \<Rightarrow> o"  (\<open>(\<open>open_block notation=\<open>prefix setclass\<close>\<close>##_)\<close> [40] 40)  where
    "setclass(A) \<equiv> \<lambda>x. x \<in> A"
 
 lemma setclass_iff [simp]: "setclass(A,x) <-> x \<in> A"
isabelle