equal
deleted
inserted
replaced
63 |
63 |
64 lemmas mini_simps = demorgans nnf_simps ex_simps all_simps |
64 lemmas mini_simps = demorgans nnf_simps ex_simps all_simps |
65 |
65 |
66 ML {* |
66 ML {* |
67 val mini_ss = simpset_of (@{context} addsimps @{thms mini_simps}); |
67 val mini_ss = simpset_of (@{context} addsimps @{thms mini_simps}); |
68 fun mini_tac ctxt = resolve_tac @{thms ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt); |
68 fun mini_tac ctxt = |
|
69 resolve_tac ctxt @{thms ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt); |
69 *} |
70 *} |
70 |
71 |
71 end |
72 end |