src/HOL/Bali/WellType.thy
changeset 61989 ba8c284d4725
parent 59807 22bc39064290
child 62042 6c6ccf573479
     1.1 --- a/src/HOL/Bali/WellType.thy	Wed Dec 30 19:41:48 2015 +0100
     1.2 +++ b/src/HOL/Bali/WellType.thy	Wed Dec 30 19:57:37 2015 +0100
     1.3 @@ -429,31 +429,31 @@
     1.4  
     1.5  (* for purely static typing *)
     1.6  abbreviation
     1.7 -  wt_syntax :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
     1.8 -  where "E|-t::T == E,empty_dt\<Turnstile>t\<Colon> T"
     1.9 +  wt_syntax :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_"  [51,51,51] 50)
    1.10 +  where "E\<turnstile>t\<Colon>T == E,empty_dt\<Turnstile>t\<Colon> T"
    1.11  
    1.12  abbreviation
    1.13 -  wt_stmt_syntax :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
    1.14 -  where "E|-s:<> == E|-In1r s :: Inl (PrimT Void)"
    1.15 +  wt_stmt_syntax :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50)
    1.16 +  where "E\<turnstile>s\<Colon>\<surd> == E\<turnstile>In1r s \<Colon> Inl (PrimT Void)"
    1.17  
    1.18  abbreviation
    1.19 -  ty_expr_syntax :: "env \<Rightarrow> [expr, ty] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
    1.20 -  where "E|-e:-T == E|-In1l e :: Inl T"
    1.21 +  ty_expr_syntax :: "env \<Rightarrow> [expr, ty] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50) 
    1.22 +  where "E\<turnstile>e\<Colon>-T == E\<turnstile>In1l e \<Colon> Inl T"
    1.23  
    1.24  abbreviation
    1.25 -  ty_var_syntax :: "env \<Rightarrow> [var, ty] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
    1.26 -  where "E|-e:=T == E|-In2 e :: Inl T"
    1.27 +  ty_var_syntax :: "env \<Rightarrow> [var, ty] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
    1.28 +  where "E\<turnstile>e\<Colon>=T == E\<turnstile>In2 e \<Colon> Inl T"
    1.29  
    1.30  abbreviation
    1.31 -  ty_exprs_syntax :: "env \<Rightarrow> [expr list, ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
    1.32 -  where "E|-e:#T == E|-In3 e :: Inr T"
    1.33 +  ty_exprs_syntax :: "env \<Rightarrow> [expr list, ty list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
    1.34 +  where "E\<turnstile>e\<Colon>\<doteq>T == E\<turnstile>In3 e \<Colon> Inr T"
    1.35  
    1.36 -notation (xsymbols)
    1.37 -  wt_syntax  ("_\<turnstile>_\<Colon>_"  [51,51,51] 50) and
    1.38 -  wt_stmt_syntax  ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50) and
    1.39 -  ty_expr_syntax  ("_\<turnstile>_\<Colon>-_" [51,51,51] 50) and
    1.40 -  ty_var_syntax  ("_\<turnstile>_\<Colon>=_" [51,51,51] 50) and
    1.41 -  ty_exprs_syntax  ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
    1.42 +notation (ASCII)
    1.43 +  wt_syntax  ("_|-_::_" [51,51,51] 50) and
    1.44 +  wt_stmt_syntax  ("_|-_:<>" [51,51   ] 50) and
    1.45 +  ty_expr_syntax  ("_|-_:-_" [51,51,51] 50) and
    1.46 +  ty_var_syntax  ("_|-_:=_" [51,51,51] 50) and
    1.47 +  ty_exprs_syntax  ("_|-_:#_" [51,51,51] 50)
    1.48  
    1.49  declare not_None_eq [simp del] 
    1.50  declare split_if [split del] split_if_asm [split del]