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