939 |
939 |
940 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] |
940 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] |
941 |
941 |
942 method_setup spy_analz = {* |
942 method_setup spy_analz = {* |
943 Method.ctxt_args (fn ctxt => |
943 Method.ctxt_args (fn ctxt => |
944 Method.SIMPLE_METHOD' (MessageSET.gen_spy_analz_tac (local_clasimpset_of ctxt))) *} |
944 SIMPLE_METHOD' (MessageSET.gen_spy_analz_tac (local_clasimpset_of ctxt))) *} |
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 (fn ctxt => |
948 Method.ctxt_args (fn ctxt => |
949 Method.SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (local_clasimpset_of ctxt))) *} |
949 SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (local_clasimpset_of ctxt))) *} |
950 "for debugging spy_analz" |
950 "for debugging spy_analz" |
951 |
951 |
952 method_setup Fake_insert_simp = {* |
952 method_setup Fake_insert_simp = {* |
953 Method.ctxt_args (fn ctxt => |
953 Method.ctxt_args (fn ctxt => |
954 Method.SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (local_simpset_of ctxt))) *} |
954 SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (local_simpset_of ctxt))) *} |
955 "for debugging spy_analz" |
955 "for debugging spy_analz" |
956 |
956 |
957 end |
957 end |