use 'datatype_new' in Quickcheck examples

--- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Wed Sep 03 00:06:19 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Wed Sep 03 00:06:21 2014 +0200
@@ -2,14 +2,16 @@
 imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
 begin
 
-datatype guest = Guest0 | Guest1
-datatype key = Key0 | Key1 | Key2 | Key3
-datatype room = Room0
+datatype_new guest = Guest0 | Guest1
+datatype_new key = Key0 | Key1 | Key2 | Key3
+datatype_new room = Room0
 
 type_synonym card = "key * key"
 
-datatype event =
-   Check_in guest room card | Enter guest room card | Exit guest room
+datatype_new event =
+  Check_in guest room card
+| Enter guest room card
+| Exit guest room
 
 definition initk :: "room \<Rightarrow> key"
   where "initk = (%r. Key0)"

--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Wed Sep 03 00:06:19 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Wed Sep 03 00:06:21 2014 +0200
@@ -122,7 +122,7 @@
 
 subsection {* Trees *}
 
-datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
+datatype_new 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
 
 primrec leaves :: "'a tree \<Rightarrow> 'a list" where
   "leaves Twig = []"
@@ -150,7 +150,7 @@
     --{* Wrong! *} 
   oops
 
-datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
+datatype_new 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
 
 primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
   "inOrder (Tip a)= [a]"
@@ -439,7 +439,7 @@
 quickcheck[random, expect = counterexample]
 oops
 
-datatype colour = Red | Green | Blue
+datatype_new colour = Red | Green | Blue
 
 record cpoint = point +
   colour :: colour

--- a/src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy	Wed Sep 03 00:06:19 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy	Wed Sep 03 00:06:21 2014 +0200
@@ -24,7 +24,7 @@
 *}
 
 text {*
-It is upto the user with which strategy the conjectures should be tested.
+It is up to the user with which strategy the conjectures should be tested.
 For example, one could check all conjectures up to a given size, and check the different conjectures in sequence.
 This is implemented by:
 *}

--- a/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy	Wed Sep 03 00:06:19 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy	Wed Sep 03 00:06:21 2014 +0200
@@ -132,7 +132,7 @@
 
 subsection {* AVL Trees *}
 
-datatype 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat
+datatype_new 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat
 
 primrec set_of :: "'a tree \<Rightarrow> 'a set"
 where
@@ -221,7 +221,7 @@
 
 declare is_ord.simps(1)[code] is_ord_mkt[code]
 
-subsubsection {* Invalid Lemma due to typo in lbal *}
+subsubsection {* Invalid Lemma due to typo in @{const l_bal} *}
 
 lemma is_ord_l_bal:
  "\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))"