946 |
946 |
947 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] |
947 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] |
948 |
948 |
949 method_setup spy_analz = {* |
949 method_setup spy_analz = {* |
950 Method.ctxt_args (fn ctxt => |
950 Method.ctxt_args (fn ctxt => |
951 Method.METHOD (fn facts => |
951 Method.SIMPLE_METHOD (gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *} |
952 gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *} |
|
953 "for proving the Fake case when analz is involved" |
952 "for proving the Fake case when analz is involved" |
954 |
953 |
955 method_setup atomic_spy_analz = {* |
954 method_setup atomic_spy_analz = {* |
956 Method.ctxt_args (fn ctxt => |
955 Method.ctxt_args (fn ctxt => |
957 Method.METHOD (fn facts => |
956 Method.SIMPLE_METHOD (atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *} |
958 atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *} |
|
959 "for debugging spy_analz" |
957 "for debugging spy_analz" |
960 |
958 |
961 method_setup Fake_insert_simp = {* |
959 method_setup Fake_insert_simp = {* |
962 Method.ctxt_args (fn ctxt => |
960 Method.ctxt_args (fn ctxt => |
963 Method.METHOD (fn facts => |
961 Method.SIMPLE_METHOD (Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *} |
964 Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *} |
|
965 "for debugging spy_analz" |
962 "for debugging spy_analz" |
966 |
963 |
967 |
964 |
968 end |
965 end |