src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy
changeset 58310 91ea607a34d8
parent 58249 180f1b3508ed
child 61671 20d4cd2ceab2
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -6,7 +6,7 @@
 
 subsection "Constant Propagation"
 
-datatype_new cval = Const val | Any
+datatype cval = Const val | Any
 
 fun rep_cval where
 "rep_cval (Const n) = {n}" |