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.METHOD (fn facts => |
939 gen_spy_analz_tac (Classical.get_local_claset ctxt, |
939 gen_spy_analz_tac (local_clasimpset_of ctxt) 1))*} |
940 Simplifier.get_local_simpset ctxt) 1))*} |
|
941 "for proving the Fake case when analz is involved" |
940 "for proving the Fake case when analz is involved" |
942 |
941 |
943 method_setup atomic_spy_analz = {* |
942 method_setup atomic_spy_analz = {* |
944 Method.ctxt_args (fn ctxt => |
943 Method.ctxt_args (fn ctxt => |
945 Method.METHOD (fn facts => |
944 Method.METHOD (fn facts => |
946 atomic_spy_analz_tac (Classical.get_local_claset ctxt, |
945 atomic_spy_analz_tac (local_clasimpset_of ctxt) 1))*} |
947 Simplifier.get_local_simpset ctxt) 1))*} |
|
948 "for debugging spy_analz" |
946 "for debugging spy_analz" |
949 |
947 |
950 method_setup Fake_insert_simp = {* |
948 method_setup Fake_insert_simp = {* |
951 Method.ctxt_args (fn ctxt => |
949 Method.ctxt_args (fn ctxt => |
952 Method.METHOD (fn facts => |
950 Method.METHOD (fn facts => |
953 Fake_insert_simp_tac (Simplifier.get_local_simpset ctxt) 1))*} |
951 Fake_insert_simp_tac (local_simpset_of ctxt) 1))*} |
954 "for debugging spy_analz" |
952 "for debugging spy_analz" |
955 |
953 |
956 |
954 |
957 end |
955 end |