1.1 --- a/src/HOL/Bali/WellType.thy	Tue Feb 09 16:07:09 2010 +0100
     1.2 +++ b/src/HOL/Bali/WellType.thy	Wed Feb 10 00:45:16 2010 +0100
     1.3 @@ -43,11 +43,9 @@
     1.4    "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
     1.5  
     1.6  
     1.7 -
     1.8 -syntax
     1.9 +abbreviation
    1.10    pkg :: "env \<Rightarrow> pname" --{* select the current package from an environment *}
    1.11 -translations 
    1.12 -  "pkg e" == "pid (cls e)"
    1.13 +  where "pkg e == pid (cls e)"
    1.14  
    1.15  section "Static overloading: maximally specific methods "
    1.16  
    1.17 @@ -426,29 +424,33 @@
    1.18                                           E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
    1.19  
    1.20  
    1.21 -syntax (* for purely static typing *)
    1.22 -  "_wt"      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
    1.23 -  "_wt_stmt" :: "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
    1.24 -  "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
    1.25 -  "_ty_var"  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
    1.26 -  "_ty_exprs":: "env \<Rightarrow> [expr list,
    1.27 -                     \<spacespace> ty   list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
    1.28 +(* for purely static typing *)
    1.29 +abbreviation
    1.30 +  wt_syntax :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
    1.31 +  where "E|-t::T == E,empty_dt\<Turnstile>t\<Colon> T"
    1.32 +
    1.33 +abbreviation
    1.34 +  wt_stmt_syntax :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
    1.35 +  where "E|-s:<> == E|-In1r s :: Inl (PrimT Void)"
    1.36 +
    1.37 +abbreviation
    1.38 +  ty_expr_syntax :: "env \<Rightarrow> [expr, ty] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
    1.39 +  where "E|-e:-T == E|-In1l e :: Inl T"
    1.40  
    1.41 -syntax (xsymbols)
    1.42 -  "_wt"      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_"  [51,51,51] 50)
    1.43 -  "_wt_stmt" ::  "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50)
    1.44 -  "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
    1.45 -  "_ty_var"  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
    1.46 -  "_ty_exprs" :: "env \<Rightarrow> [expr list,
    1.47 -                    \<spacespace>  ty   list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
    1.48 +abbreviation
    1.49 +  ty_var_syntax :: "env \<Rightarrow> [var, ty] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
    1.50 +  where "E|-e:=T == E|-In2 e :: Inl T"
    1.51  
    1.52 -translations
    1.53 -        "E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T"
    1.54 -        "E\<turnstile>s\<Colon>\<surd>"  == "E\<turnstile>In1r s\<Colon>CONST Inl (PrimT Void)"
    1.55 -        "E\<turnstile>e\<Colon>-T" == "E\<turnstile>In1l e\<Colon>CONST Inl T"
    1.56 -        "E\<turnstile>e\<Colon>=T" == "E\<turnstile>In2  e\<Colon>CONST Inl T"
    1.57 -        "E\<turnstile>e\<Colon>\<doteq>T" == "E\<turnstile>In3  e\<Colon>CONST Inr T"
    1.58 +abbreviation
    1.59 +  ty_exprs_syntax :: "env \<Rightarrow> [expr list, ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
    1.60 +  where "E|-e:#T == E|-In3 e :: Inr T"
    1.61  
    1.62 +notation (xsymbols)
    1.63 +  wt_syntax  ("_\<turnstile>_\<Colon>_"  [51,51,51] 50) and
    1.64 +  wt_stmt_syntax  ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50) and
    1.65 +  ty_expr_syntax  ("_\<turnstile>_\<Colon>-_" [51,51,51] 50) and
    1.66 +  ty_var_syntax  ("_\<turnstile>_\<Colon>=_" [51,51,51] 50) and
    1.67 +  ty_exprs_syntax  ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
    1.68  
    1.69  declare not_None_eq [simp del] 
    1.70  declare split_if [split del] split_if_asm [split del]