# HG changeset patch
# User wenzelm
# Date 854012421 -3600
# Node ID ddd22ceee8cc17b7d3e3bb7b266387022aff6298
# Parent  c55f68761a8df0994f8ae1f099d62ba16b8adaf7
turned some consts into syntax;

diff -r c55f68761a8d -r ddd22ceee8cc src/ZF/Bool.thy
--- a/src/ZF/Bool.thy	Thu Jan 23 10:35:28 1997 +0100
+++ b/src/ZF/Bool.thy	Thu Jan 23 10:40:21 1997 +0100
@@ -10,8 +10,6 @@
 
 Bool = upair + 
 consts
-    "1"         :: i             ("1")
-    "2"         :: i             ("2")
     bool        :: i
     cond        :: [i,i,i]=>i
     not         :: i=>i
@@ -19,6 +17,10 @@
     or          :: [i,i]=>i      (infixl 65)
     xor         :: [i,i]=>i      (infixl 65)
 
+syntax
+    "1"         :: i             ("1")
+    "2"         :: i             ("2")
+
 translations
    "1"  == "succ(0)"
    "2"  == "succ(1)"
diff -r c55f68761a8d -r ddd22ceee8cc src/ZF/List.thy
--- a/src/ZF/List.thy	Thu Jan 23 10:35:28 1997 +0100
+++ b/src/ZF/List.thy	Thu Jan 23 10:40:21 1997 +0100
@@ -13,17 +13,16 @@
 List = Datatype + 
 
 consts
- (* List Enumeration *)
- "[]"        :: i                                       ("[]")
- "@List"     :: is => i                                 ("[(_)]")
-
   list       :: i=>i
-
   
 datatype
   "list(A)" = Nil | Cons ("a:A", "l: list(A)")
 
 
+syntax
+ "[]"        :: i                                       ("[]")
+ "@List"     :: is => i                                 ("[(_)]")
+
 translations
   "[x, xs]"     == "Cons(x, [xs])"
   "[x]"         == "Cons(x, [])"
diff -r c55f68761a8d -r ddd22ceee8cc src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Thu Jan 23 10:35:28 1997 +0100
+++ b/src/ZF/Ordinal.thy	Thu Jan 23 10:40:21 1997 +0100
@@ -11,8 +11,10 @@
   Memrel        :: i=>i
   Transset,Ord  :: i=>o
   "<"           :: [i,i] => o  (infixl 50) (*less than on ordinals*)
+  Limit         :: i=>o
+
+syntax
   "le"          :: [i,i] => o  (infixl 50) (*less than or equals*)
-  Limit         :: i=>o
 
 translations
   "x le y"      == "x < succ(y)"