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/Library/FSet.thy
changeset 80768 c7723cc15de8
parent 80285 8678986d9af5
child 80786 70076ba563d2
child 80790 07c51801c2ea 
--- a/src/HOL/Library/FSet.thy	Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Library/FSet.thy	Sun Aug 25 21:10:01 2024 +0200
@@ -167,6 +167,9 @@
 syntax
   "_insert_fset"     :: "args => 'a fset"  ("{|(_)|}")
 
+syntax_consts
+  "_insert_fset" == finsert
+
 translations
   "{|x, xs|}" == "CONST finsert x {|xs|}"
   "{|x|}"     == "CONST finsert x {||}"
@@ -200,6 +203,10 @@
   "_fBall"       :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>(_/|\<in>|_)./ _)" [0, 0, 10] 10)
   "_fBex"        :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>(_/|\<in>|_)./ _)" [0, 0, 10] 10)
 
+syntax_consts
+  "_fBall" \<rightleftharpoons> FSet.Ball and
+  "_fBex" \<rightleftharpoons> FSet.Bex
+
 translations
   "\<forall>x|\<in>|A. P" \<rightleftharpoons> "CONST FSet.Ball A (\<lambda>x. P)"
   "\<exists>x|\<in>|A. P" \<rightleftharpoons> "CONST FSet.Bex A (\<lambda>x. P)"
isabelle