| changeset 26341 | 2f5a4367a39e |
| parent 24958 | ff15f76741bd |
| child 29265 | 5b4247055bd7 |
--- a/src/HOL/Tools/cnf_funcs.ML Wed Mar 19 22:47:38 2008 +0100 +++ b/src/HOL/Tools/cnf_funcs.ML Wed Mar 19 22:47:39 2008 +0100 @@ -54,7 +54,7 @@ struct fun thm_by_auto (G : string) : thm = - prove_goal (the_context ()) G (fn prems => [cut_facts_tac prems 1, Auto_tac]); + prove_goal (the_context ()) G (fn prems => [cut_facts_tac prems 1, CLASIMPSET auto_tac]); (* Thm.thm *) val clause2raw_notE = thm_by_auto "[| P; ~P |] ==> False";