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