| changeset 58249 | 180f1b3508ed |
| parent 45111 | 054a9ac0d7ef |
| child 58310 | 91ea607a34d8 |
--- a/src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy Tue Sep 09 20:51:36 2014 +0200 @@ -10,7 +10,7 @@ text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *} -datatype 'a astate = FunDom "string \<Rightarrow> 'a" "string list" +datatype_new 'a astate = FunDom "string \<Rightarrow> 'a" "string list" fun "fun" where "fun (FunDom f _) = f" fun dom where "dom (FunDom _ A) = A"