# HG changeset patch
# User berghofe
# Date 1210150612 -7200
# Node ID 0af0f674845d2492af9a033b0bc689976605e956
# Parent  9eede540a5e86fe5bd652000a7c633c357e853a1
- Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
  to_set and to_pred attributes, because it is no longer applied automatically
- Manually applied predicate1I in proof of accp_subset, because it is no longer
  part of the claset
- Replaced psubset_def by less_le

diff -r 9eede540a5e8 -r 0af0f674845d src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Wed May 07 10:56:50 2008 +0200
+++ b/src/HOL/Wellfounded.thy	Wed May 07 10:56:52 2008 +0200
@@ -271,7 +271,7 @@
 done
 
 lemmas wfP_SUP = wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}",
-  to_pred SUP_UN_eq2 bot_empty_eq, simplified, standard]
+  to_pred SUP_UN_eq2 bot_empty_eq pred_equals_eq, simplified, standard]
 
 lemma wf_Union: 
  "[| ALL r:R. wf r;  
@@ -691,7 +691,7 @@
 lemma accp_subset:
   assumes sub: "R1 \<le> R2"
   shows "accp R2 \<le> accp R1"
-proof
+proof (rule predicate1I)
   fix x assume "accp R2 x"
   then show "accp R1 x"
   proof (induct x)
@@ -745,9 +745,9 @@
 
 lemmas wf_acc_iff = wfP_accp_iff [to_set]
 
-lemmas acc_subset = accp_subset [to_set]
+lemmas acc_subset = accp_subset [to_set pred_subset_eq]
 
-lemmas acc_subset_induct = accp_subset_induct [to_set]
+lemmas acc_subset_induct = accp_subset_induct [to_set pred_subset_eq]
 
 
 subsection {* Tools for building wellfounded relations *}
@@ -837,7 +837,7 @@
 done
 
 lemma trans_finite_psubset: "trans finite_psubset"
-by (simp add: finite_psubset_def psubset_def trans_def, blast)
+by (simp add: finite_psubset_def less_le trans_def, blast)