equal
deleted
inserted
replaced
939 |
939 |
940 lemma Fake_parts_sing: |
940 lemma Fake_parts_sing: |
941 "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H"; |
941 "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H"; |
942 apply (rule subset_trans) |
942 apply (rule subset_trans) |
943 apply (erule_tac [2] Fake_parts_insert) |
943 apply (erule_tac [2] Fake_parts_insert) |
944 apply (rule parts_mono) |
944 apply (rule parts_mono, blast) |
945 apply (blast intro: elim:); |
|
946 done |
945 done |
947 |
946 |
948 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] |
947 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] |
949 |
948 |
950 method_setup spy_analz = {* |
949 method_setup spy_analz = {* |