turned some consts into syntax;
authorwenzelm
Thu Jan 23 10:40:21 1997 +0100 (1997-01-23)
changeset 2539ddd22ceee8cc
parent 2538 c55f68761a8d
child 2540 ba8311047f18
turned some consts into syntax;
src/ZF/Bool.thy
src/ZF/List.thy
src/ZF/Ordinal.thy
     1.1 --- a/src/ZF/Bool.thy	Thu Jan 23 10:35:28 1997 +0100
     1.2 +++ b/src/ZF/Bool.thy	Thu Jan 23 10:40:21 1997 +0100
     1.3 @@ -10,8 +10,6 @@
     1.4  
     1.5  Bool = upair + 
     1.6  consts
     1.7 -    "1"         :: i             ("1")
     1.8 -    "2"         :: i             ("2")
     1.9      bool        :: i
    1.10      cond        :: [i,i,i]=>i
    1.11      not         :: i=>i
    1.12 @@ -19,6 +17,10 @@
    1.13      or          :: [i,i]=>i      (infixl 65)
    1.14      xor         :: [i,i]=>i      (infixl 65)
    1.15  
    1.16 +syntax
    1.17 +    "1"         :: i             ("1")
    1.18 +    "2"         :: i             ("2")
    1.19 +
    1.20  translations
    1.21     "1"  == "succ(0)"
    1.22     "2"  == "succ(1)"
     2.1 --- a/src/ZF/List.thy	Thu Jan 23 10:35:28 1997 +0100
     2.2 +++ b/src/ZF/List.thy	Thu Jan 23 10:40:21 1997 +0100
     2.3 @@ -13,17 +13,16 @@
     2.4  List = Datatype + 
     2.5  
     2.6  consts
     2.7 - (* List Enumeration *)
     2.8 - "[]"        :: i                                       ("[]")
     2.9 - "@List"     :: is => i                                 ("[(_)]")
    2.10 -
    2.11    list       :: i=>i
    2.12 -
    2.13    
    2.14  datatype
    2.15    "list(A)" = Nil | Cons ("a:A", "l: list(A)")
    2.16  
    2.17  
    2.18 +syntax
    2.19 + "[]"        :: i                                       ("[]")
    2.20 + "@List"     :: is => i                                 ("[(_)]")
    2.21 +
    2.22  translations
    2.23    "[x, xs]"     == "Cons(x, [xs])"
    2.24    "[x]"         == "Cons(x, [])"
     3.1 --- a/src/ZF/Ordinal.thy	Thu Jan 23 10:35:28 1997 +0100
     3.2 +++ b/src/ZF/Ordinal.thy	Thu Jan 23 10:40:21 1997 +0100
     3.3 @@ -11,8 +11,10 @@
     3.4    Memrel        :: i=>i
     3.5    Transset,Ord  :: i=>o
     3.6    "<"           :: [i,i] => o  (infixl 50) (*less than on ordinals*)
     3.7 +  Limit         :: i=>o
     3.8 +
     3.9 +syntax
    3.10    "le"          :: [i,i] => o  (infixl 50) (*less than or equals*)
    3.11 -  Limit         :: i=>o
    3.12  
    3.13  translations
    3.14    "x le y"      == "x < succ(y)"