# HG changeset patch
# User berghofe
# Date 1326215523 -3600
# Node ID 1898e61e89c497f8174d30975fd40b8e6320469b
# Parent  48c534b220403c5fd7c86353d84f099239e0be8d
pred_subset/equals_eq are now standard pred_set_conv rules

diff -r 48c534b22040 -r 1898e61e89c4 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Jan 10 18:09:09 2012 +0100
+++ b/src/HOL/List.thy	Tue Jan 10 18:12:03 2012 +0100
@@ -4559,7 +4559,7 @@
 lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
 by (rule predicate1I, erule listsp.induct, (blast dest: predicate1D)+)
 
-lemmas lists_mono = listsp_mono [to_set pred_subset_eq]
+lemmas lists_mono = listsp_mono [to_set]
 
 lemma listsp_infI:
   assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
@@ -4575,7 +4575,7 @@
 
 lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_def inf_bool_def]
 
-lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set pred_equals_eq]
+lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set]
 
 lemma Cons_in_lists_iff[simp]: "x#xs : lists A \<longleftrightarrow> x:A \<and> xs : lists A"
 by auto