equal
deleted
inserted
replaced
917 done |
917 done |
918 |
918 |
919 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] |
919 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] |
920 |
920 |
921 method_setup spy_analz = {* |
921 method_setup spy_analz = {* |
922 Method.ctxt_args (fn ctxt => |
922 Method.ctxt_args (SIMPLE_METHOD' o gen_spy_analz_tac o local_clasimpset_of) *} |
923 Method.SIMPLE_METHOD (gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *} |
|
924 "for proving the Fake case when analz is involved" |
923 "for proving the Fake case when analz is involved" |
925 |
924 |
926 method_setup atomic_spy_analz = {* |
925 method_setup atomic_spy_analz = {* |
927 Method.ctxt_args (fn ctxt => |
926 Method.ctxt_args (SIMPLE_METHOD' o atomic_spy_analz_tac o local_clasimpset_of) *} |
928 Method.SIMPLE_METHOD (atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *} |
|
929 "for debugging spy_analz" |
927 "for debugging spy_analz" |
930 |
928 |
931 method_setup Fake_insert_simp = {* |
929 method_setup Fake_insert_simp = {* |
932 Method.ctxt_args (fn ctxt => |
930 Method.ctxt_args (SIMPLE_METHOD' o Fake_insert_simp_tac o local_simpset_of) *} |
933 Method.SIMPLE_METHOD (Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *} |
|
934 "for debugging spy_analz" |
931 "for debugging spy_analz" |
935 |
932 |
936 |
933 |
937 end |
934 end |
938 (*>*) |
935 (*>*) |