equal
deleted
inserted
replaced
52 |
52 |
53 structure cnf : CNF = |
53 structure cnf : CNF = |
54 struct |
54 struct |
55 |
55 |
56 fun thm_by_auto (G : string) : thm = |
56 fun thm_by_auto (G : string) : thm = |
57 prove_goal (the_context ()) G (fn prems => [cut_facts_tac prems 1, Auto_tac]); |
57 prove_goal (the_context ()) G (fn prems => [cut_facts_tac prems 1, CLASIMPSET auto_tac]); |
58 |
58 |
59 (* Thm.thm *) |
59 (* Thm.thm *) |
60 val clause2raw_notE = thm_by_auto "[| P; ~P |] ==> False"; |
60 val clause2raw_notE = thm_by_auto "[| P; ~P |] ==> False"; |
61 val clause2raw_not_disj = thm_by_auto "[| ~P; ~Q |] ==> ~(P | Q)"; |
61 val clause2raw_not_disj = thm_by_auto "[| ~P; ~Q |] ==> ~(P | Q)"; |
62 val clause2raw_not_not = thm_by_auto "P ==> ~~P"; |
62 val clause2raw_not_not = thm_by_auto "P ==> ~~P"; |