| changeset 45212 | e87feee00a4c |
| parent 45200 | 1f1897ac7877 |
| child 52046 | bc01725d7918 |
--- a/src/HOL/IMP/Poly_Types.thy Wed Oct 19 23:07:48 2011 +0200 +++ b/src/HOL/IMP/Poly_Types.thy Thu Oct 20 09:48:00 2011 +0200 @@ -6,7 +6,7 @@ text{* Everything else remains the same. *} -type_synonym tyenv = "name \<Rightarrow> ty" +type_synonym tyenv = "vname \<Rightarrow> ty" inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool" ("(1_/ \<turnstile>p/ (_ :/ _))" [50,0,50] 50)