src/HOL/MetisExamples/set.thy
changeset 32519 e9644b497e1c
parent 28592 824f8390aaa2
child 32685 29e4e567b5f4
     1.1 --- a/src/HOL/MetisExamples/set.thy	Thu Sep 03 22:48:18 2009 +0200
     1.2 +++ b/src/HOL/MetisExamples/set.thy	Fri Sep 04 15:18:35 2009 +0200
     1.3 @@ -238,7 +238,7 @@
     1.4  
     1.5  lemma (*singleton_example_2:*)
     1.6       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
     1.7 -by (metis Un_absorb2 Union_insert insertI1 insert_Diff insert_Diff_single subset_eq)
     1.8 +by (metis Set.subsetI Union_upper insert_code mem_def set_eq_subset)
     1.9  
    1.10  lemma singleton_example_2:
    1.11       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
    1.12 @@ -275,8 +275,8 @@
    1.13  apply (metis emptyE)
    1.14  apply (metis insert_iff singletonE)
    1.15  apply (metis insertCI singletonE zless_le)
    1.16 -apply (metis insert_iff singletonE)
    1.17 -apply (metis insert_iff singletonE)
    1.18 +apply (metis Collect_def Collect_mem_eq)
    1.19 +apply (metis Collect_def Collect_mem_eq)
    1.20  apply (metis DiffE)
    1.21  apply (metis pair_in_Id_conv) 
    1.22  done