pred_subset/equals_eq are now standard pred_set_conv rules
authorberghofe
Tue Jan 10 18:12:03 2012 +0100 (2012-01-10)
changeset 461761898e61e89c4
parent 46175 48c534b22040
child 46177 adac34829e10
pred_subset/equals_eq are now standard pred_set_conv rules
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Tue Jan 10 18:09:09 2012 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Jan 10 18:12:03 2012 +0100
     1.3 @@ -4559,7 +4559,7 @@
     1.4  lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
     1.5  by (rule predicate1I, erule listsp.induct, (blast dest: predicate1D)+)
     1.6  
     1.7 -lemmas lists_mono = listsp_mono [to_set pred_subset_eq]
     1.8 +lemmas lists_mono = listsp_mono [to_set]
     1.9  
    1.10  lemma listsp_infI:
    1.11    assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
    1.12 @@ -4575,7 +4575,7 @@
    1.13  
    1.14  lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_def inf_bool_def]
    1.15  
    1.16 -lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set pred_equals_eq]
    1.17 +lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set]
    1.18  
    1.19  lemma Cons_in_lists_iff[simp]: "x#xs : lists A \<longleftrightarrow> x:A \<and> xs : lists A"
    1.20  by auto