Mercurialisabelle / diff
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/HOL/Bali/WellType.thy
changeset 24783 5a3e336a2e37
parent 24019 67bde7cfcf10
child 27208 5fe899199f85 
     1.1 --- a/src/HOL/Bali/WellType.thy	Sun Sep 30 16:53:08 2007 +0200
     1.2 +++ b/src/HOL/Bali/WellType.thy	Sun Sep 30 21:55:15 2007 +0200
     1.3 @@ -426,19 +426,19 @@
     1.4  
     1.5  
     1.6  syntax (* for purely static typing *)
     1.7 -  wt_      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
     1.8 -  wt_stmt_ :: "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
     1.9 -  ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
    1.10 -  ty_var_  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
    1.11 -  ty_exprs_:: "env \<Rightarrow> [expr list,
    1.12 +  "_wt"      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
    1.13 +  "_wt_stmt" :: "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
    1.14 +  "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
    1.15 +  "_ty_var"  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
    1.16 +  "_ty_exprs":: "env \<Rightarrow> [expr list,
    1.17  		     \<spacespace> ty   list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
    1.18  
    1.19  syntax (xsymbols)
    1.20 -  wt_      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_"  [51,51,51] 50)
    1.21 -  wt_stmt_ ::  "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50)
    1.22 -  ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
    1.23 -  ty_var_  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
    1.24 -  ty_exprs_ :: "env \<Rightarrow> [expr list,
    1.25 +  "_wt"      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_"  [51,51,51] 50)
    1.26 +  "_wt_stmt" ::  "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50)
    1.27 +  "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
    1.28 +  "_ty_var"  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
    1.29 +  "_ty_exprs" :: "env \<Rightarrow> [expr list,
    1.30  		    \<spacespace>  ty   list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
    1.31  
    1.32  translations
isabelle