Mercurial Mercurial > hg > nominal2 / 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.
infix for In
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 21 Apr 2010 12:25:52 +0200
changeset 1951 a0c7290a4e27
parent 1916 c8b31085cb5b
child 1952 27cdc0a3a763
infix for In
Nominal/FSet.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/FSet.thy	Wed Apr 21 10:24:39 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 21 12:25:52 2010 +0200
@@ -370,7 +370,7 @@
   "{|x|}"     == "CONST finsert x {||}"
 
 quotient_definition
-  fin ("_ |\<in>| _" [50, 51] 50)
+  fin (infix "|\<in>|" 50)
 where
   "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb"
nominal2