src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy

   by (induct xs) simp_all
 
 
 subsection {* Trees *}
 
-datatype_new 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
+datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
 
 primrec leaves :: "'a tree \<Rightarrow> 'a list" where
   "leaves Twig = []"
   | "leaves (Leaf a) = [a]"
   | "leaves (Branch l r) = (leaves l) @ (leaves r)"

   quickcheck[random, expect = counterexample]
   quickcheck[exhaustive, expect = counterexample]
     --{* Wrong! *} 
   oops
 
-datatype_new 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
+datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
 
 primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
   "inOrder (Tip a)= [a]"
   | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
 

   "xpos r = xpos r' ==> r = r'"
 quickcheck[exhaustive, expect = counterexample]
 quickcheck[random, expect = counterexample]
 oops
 
-datatype_new colour = Red | Green | Blue
+datatype colour = Red | Green | Blue
 
 record cpoint = point +
   colour :: colour
 
 lemma