equal
deleted
inserted
replaced
939 done |
939 done |
940 |
940 |
941 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] |
941 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] |
942 |
942 |
943 method_setup spy_analz = {* |
943 method_setup spy_analz = {* |
944 Method.ctxt_args (SIMPLE_METHOD' o Message.gen_spy_analz_tac o local_clasimpset_of) *} |
944 Scan.succeed (SIMPLE_METHOD' o Message.gen_spy_analz_tac o local_clasimpset_of) *} |
945 "for proving the Fake case when analz is involved" |
945 "for proving the Fake case when analz is involved" |
946 |
946 |
947 method_setup atomic_spy_analz = {* |
947 method_setup atomic_spy_analz = {* |
948 Method.ctxt_args (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o local_clasimpset_of) *} |
948 Scan.succeed (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o local_clasimpset_of) *} |
949 "for debugging spy_analz" |
949 "for debugging spy_analz" |
950 |
950 |
951 method_setup Fake_insert_simp = {* |
951 method_setup Fake_insert_simp = {* |
952 Method.ctxt_args (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o local_simpset_of) *} |
952 Scan.succeed (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o local_simpset_of) *} |
953 "for debugging spy_analz" |
953 "for debugging spy_analz" |
954 |
954 |
955 end |
955 end |