src/HOL/IMP/Abs_State.thy
changeset 45212 e87feee00a4c
parent 45127 d2eb07a1e01b
child 45623 f682f3f7b726
     1.1 --- a/src/HOL/IMP/Abs_State.thy	Wed Oct 19 23:07:48 2011 +0200
     1.2 +++ b/src/HOL/IMP/Abs_State.thy	Thu Oct 20 09:48:00 2011 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
     1.6  
     1.7 -datatype 'a st = FunDom "name \<Rightarrow> 'a" "name list"
     1.8 +datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname list"
     1.9  
    1.10  fun "fun" where "fun (FunDom f _) = f"
    1.11  fun dom where "dom (FunDom _ A) = A"