src/HOL/Bali/WellType.thy
changeset 35431 8758fe1fc9f8
parent 35416 d8d7d1b785af
child 36367 49c7dee21a7f
     1.1 --- a/src/HOL/Bali/WellType.thy	Wed Mar 03 00:32:14 2010 +0100
     1.2 +++ b/src/HOL/Bali/WellType.thy	Wed Mar 03 00:33:02 2010 +0100
     1.3 @@ -37,10 +37,10 @@
     1.4           lcl:: "lenv"    --{* local environment *}     
     1.5    
     1.6  translations
     1.7 -  "lenv" <= (type) "(lname, ty) table"
     1.8 -  "lenv" <= (type) "lname \<Rightarrow> ty option"
     1.9 -  "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
    1.10 -  "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
    1.11 +  (type) "lenv" <= (type) "(lname, ty) table"
    1.12 +  (type) "lenv" <= (type) "lname \<Rightarrow> ty option"
    1.13 +  (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
    1.14 +  (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
    1.15  
    1.16  
    1.17  abbreviation
    1.18 @@ -238,9 +238,9 @@
    1.19  
    1.20  section "Typing for terms"
    1.21  
    1.22 -types tys  =        "ty + ty list"
    1.23 +types tys  = "ty + ty list"
    1.24  translations
    1.25 -  "tys"   <= (type) "ty + ty list"
    1.26 +  (type) "tys" <= (type) "ty + ty list"
    1.27  
    1.28  
    1.29  inductive