| changeset 49490 | 394870e51d18 |
| parent 49488 | 02eb07152998 |
| child 49504 | df9b897fb254 |
--- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Fri Sep 21 11:44:55 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Fri Sep 21 11:51:07 2012 +0200 @@ -56,7 +56,6 @@ val o_eq_dest_lhs = @{thm o_eq_dest_lhs}; val ordIso_transitive = @{thm ordIso_transitive}; val ordLeq_csum2 = @{thm ordLeq_csum2}; -val subset_UNIV = @{thm subset_UNIV}; val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]}; val trans_o_apply = @{thm trans[OF o_apply]};