| changeset 49344 | ce1ccb78ecda |
| parent 47619 | 0d3e95375bb7 |
| child 49353 | 023be49d7fb8 |
--- a/src/HOL/IMP/Abs_State.thy Wed Sep 12 23:38:12 2012 +0200 +++ b/src/HOL/IMP/Abs_State.thy Thu Sep 13 10:28:48 2012 +0200 @@ -99,8 +99,8 @@ datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname set" -fun "fun" where "fun (FunDom f xs) = f" -fun dom where "dom (FunDom f xs) = xs" +fun "fun" where "fun (FunDom f X) = f" +fun dom where "dom (FunDom f X) = X" definition "show_st S = (\<lambda>x. (x, fun S x)) ` dom S"