src/ZF/OrderType.thy
changeset 1401 0c439768f45c
parent 1033 437728256de3
child 1478 2b8c2a7547ab
--- a/src/ZF/OrderType.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/OrderType.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -10,14 +10,14 @@
 
 OrderType = OrderArith + Ordinal + 
 consts
-  ordermap  :: "[i,i]=>i"
-  ordertype :: "[i,i]=>i"
+  ordermap  :: [i,i]=>i
+  ordertype :: [i,i]=>i
 
-  Ord_alt   :: "i => o"   
+  Ord_alt   :: i => o   
 
-  "**"      :: "[i,i]=>i"           (infixl 70)
-  "++"      :: "[i,i]=>i"           (infixl 65)
-  "--"      :: "[i,i]=>i"           (infixl 65)
+  "**"      :: [i,i]=>i           (infixl 70)
+  "++"      :: [i,i]=>i           (infixl 65)
+  "--"      :: [i,i]=>i           (infixl 65)
  
 
 defs