# HG changeset patch
# User paulson
# Date 1012389779 -3600
# Node ID 7ec4807b53cf0b0edd326c908c47b0fc294f70f1
# Parent  7fc3fbfed8ef43a80abd0d926b8e61383e13f27d
mu-syntax for the LEAST operator

diff -r 7fc3fbfed8ef -r 7ec4807b53cf src/ZF/Cardinal.thy
--- 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