# HG changeset patch
# User huffman
# Date 1289937430 28800
# Node ID fa5e0cacd5e712ad8f2dda336a52dbe308c4ec7e
# Parent  b9a86f15e7638292880127e381dc2438d6eea605
declare {upper,lower,convex}_pd_induct as default induction rules

diff -r b9a86f15e763 -r fa5e0cacd5e7 src/HOLCF/ConvexPD.thy
--- 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)"
diff -r b9a86f15e763 -r fa5e0cacd5e7 src/HOLCF/LowerPD.thy
--- 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)"
diff -r b9a86f15e763 -r fa5e0cacd5e7 src/HOLCF/UpperPD.thy
--- 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)"