933 |
933 |
934 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] |
934 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] |
935 |
935 |
936 method_setup spy_analz = {* |
936 method_setup spy_analz = {* |
937 Method.ctxt_args (fn ctxt => |
937 Method.ctxt_args (fn ctxt => |
938 Method.METHOD (fn facts => |
938 Method.SIMPLE_METHOD' (gen_spy_analz_tac (local_clasimpset_of ctxt))) *} |
939 gen_spy_analz_tac (local_clasimpset_of ctxt) 1))*} |
|
940 "for proving the Fake case when analz is involved" |
939 "for proving the Fake case when analz is involved" |
941 |
940 |
942 method_setup atomic_spy_analz = {* |
941 method_setup atomic_spy_analz = {* |
943 Method.ctxt_args (fn ctxt => |
942 Method.ctxt_args (fn ctxt => |
944 Method.METHOD (fn facts => |
943 Method.SIMPLE_METHOD' (atomic_spy_analz_tac (local_clasimpset_of ctxt))) *} |
945 atomic_spy_analz_tac (local_clasimpset_of ctxt) 1))*} |
|
946 "for debugging spy_analz" |
944 "for debugging spy_analz" |
947 |
945 |
948 method_setup Fake_insert_simp = {* |
946 method_setup Fake_insert_simp = {* |
949 Method.ctxt_args (fn ctxt => |
947 Method.ctxt_args (fn ctxt => |
950 Method.METHOD (fn facts => |
948 Method.SIMPLE_METHOD' (Fake_insert_simp_tac (local_simpset_of ctxt))) *} |
951 Fake_insert_simp_tac (local_simpset_of ctxt) 1))*} |
|
952 "for debugging spy_analz" |
949 "for debugging spy_analz" |
953 |
950 |
954 |
|
955 end |
951 end |