equal
deleted
inserted
replaced
58 "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))", |
58 "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))", |
59 "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q", |
59 "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q", |
60 "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))"]; |
60 "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))"]; |
61 |
61 |
62 |
62 |
63 val mini_ss = |
63 val mini_ss=FOL_basic_ss addsimps (demorgans @ nnf_simps @ ex_simps @ all_simps); |
64 empty_ss |
|
65 setmksimps (map mk_meta_eq o atomize o gen_all) |
|
66 setsolver (fn prems => resolve_tac (triv_rls@prems) |
|
67 ORELSE' assume_tac |
|
68 ORELSE' etac FalseE) |
|
69 setsubgoaler asm_simp_tac |
|
70 addsimps (demorgans @ nnf_simps @ ex_simps @ all_simps); |
|
71 |
64 |
72 val mini_tac = rtac ccontr THEN' asm_full_simp_tac mini_ss; |
65 val mini_tac = rtac ccontr THEN' asm_full_simp_tac mini_ss; |
73 |
66 |