src/HOL/Enum.thy

 
 subsection {* Small finite types *}
 
 text {* We define small finite types for the use in Quickcheck *}
 
-datatype_new finite_1 = a\<^sub>1
+datatype finite_1 = a\<^sub>1
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
 
 lemma UNIV_finite_1:
   "UNIV = {a\<^sub>1}"

 end
 
 declare [[simproc del: finite_1_eq]]
 hide_const (open) a\<^sub>1
 
-datatype_new finite_2 = a\<^sub>1 | a\<^sub>2
+datatype finite_2 = a\<^sub>1 | a\<^sub>2
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
 notation (output) a\<^sub>2  ("a\<^sub>2")
 
 lemma UNIV_finite_2:

      split: finite_2.splits)
 end
 
 hide_const (open) a\<^sub>1 a\<^sub>2
 
-datatype_new finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
+datatype finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
 notation (output) a\<^sub>2  ("a\<^sub>2")
 notation (output) a\<^sub>3  ("a\<^sub>3")
 

      split: finite_3.splits)
 end
 
 hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
 
-datatype_new finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
+datatype finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
 notation (output) a\<^sub>2  ("a\<^sub>2")
 notation (output) a\<^sub>3  ("a\<^sub>3")
 notation (output) a\<^sub>4  ("a\<^sub>4")

 end
 
 hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
 
 
-datatype_new finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
+datatype finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
 notation (output) a\<^sub>2  ("a\<^sub>2")
 notation (output) a\<^sub>3  ("a\<^sub>3")
 notation (output) a\<^sub>4  ("a\<^sub>4")