declare {upper,lower,convex}_pd_induct as default induction rules

--- a/src/HOLCF/ConvexPD.thy	Tue Nov 16 11:50:05 2010 -0800
+++ b/src/HOLCF/ConvexPD.thy	Tue Nov 16 11:57:10 2010 -0800
@@ -289,7 +289,8 @@
 apply (erule insert [OF unit])
 done
 
-lemma convex_pd_induct:
+lemma convex_pd_induct
+  [case_names adm convex_unit convex_plus, induct type: convex_pd]:
   assumes P: "adm P"
   assumes unit: "\<And>x. P {x}\<natural>"
   assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<natural> ys)"

--- a/src/HOLCF/LowerPD.thy	Tue Nov 16 11:50:05 2010 -0800
+++ b/src/HOLCF/LowerPD.thy	Tue Nov 16 11:57:10 2010 -0800
@@ -281,7 +281,8 @@
 apply (erule insert [OF unit])
 done
 
-lemma lower_pd_induct:
+lemma lower_pd_induct
+  [case_names adm lower_unit lower_plus, induct type: lower_pd]:
   assumes P: "adm P"
   assumes unit: "\<And>x. P {x}\<flat>"
   assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<flat> ys)"

--- a/src/HOLCF/UpperPD.thy	Tue Nov 16 11:50:05 2010 -0800
+++ b/src/HOLCF/UpperPD.thy	Tue Nov 16 11:57:10 2010 -0800
@@ -276,7 +276,8 @@
 apply (erule insert [OF unit])
 done
 
-lemma upper_pd_induct:
+lemma upper_pd_induct
+  [case_names adm upper_unit upper_plus, induct type: upper_pd]:
   assumes P: "adm P"
   assumes unit: "\<And>x. P {x}\<sharp>"
   assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<sharp> ys)"