equal
deleted
inserted
replaced
62 by blast+ |
62 by blast+ |
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} addsimps @{thms mini_simps}; |
67 val mini_ss = simpset_of (@{context} addsimps @{thms mini_simps}); |
68 val mini_tac = rtac @{thm ccontr} THEN' asm_full_simp_tac mini_ss; |
68 fun mini_tac ctxt = rtac @{thm ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt); |
69 *} |
69 *} |
70 |
70 |
71 end |
71 end |