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/Cardinal.thy
changeset 1401 0c439768f45c
parent 832 ad50a9e74eaf
child 1478 2b8c2a7547ab 
--- a/src/ZF/Cardinal.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Cardinal.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,11 +8,11 @@
 
 Cardinal = OrderType + Fixedpt + Nat + Sum + 
 consts
-  Least            :: "(i=>o) => i"    (binder "LEAST " 10)
+  Least            :: (i=>o) => i    (binder "LEAST " 10)
   eqpoll, lepoll,
-          lesspoll :: "[i,i] => o"     (infixl 50)
-  cardinal         :: "i=>i"           ("|_|")
-  Finite, Card     :: "i=>o"
+          lesspoll :: [i,i] => o     (infixl 50)
+  cardinal         :: i=>i           ("|_|")
+  Finite, Card     :: i=>o
 
 defs
isabelle