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