Mercurial Mercurial > repos > isabelle / 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.
mu-syntax for the LEAST operator
authorpaulson
Wed, 30 Jan 2002 12:22:59 +0100
changeset 12861 7ec4807b53cf
parent 12860 7fc3fbfed8ef
child 12862 c66cb5591191
mu-syntax for the LEAST operator
src/ZF/Cardinal.thy file | annotate | diff | comparison | revisions 
--- a/src/ZF/Cardinal.thy	Wed Jan 30 12:22:40 2002 +0100
+++ b/src/ZF/Cardinal.thy	Wed Jan 30 12:22:59 2002 +0100
@@ -35,5 +35,6 @@
   "op eqpoll"      :: [i,i] => o     (infixl "\\<approx>" 50)
   "op lepoll"      :: [i,i] => o     (infixl "\\<lesssim>" 50)
   "op lesspoll"    :: [i,i] => o     (infixl "\\<prec>" 50)
+  "LEAST "         :: [pttrn, o] => i        ("(3\\<mu>_./ _)" [0, 10] 10)
 
 end
isabelle