| changeset 14749 | 9ccfd0f59e11 |
| parent 14430 | 5cb24165a2e1 |
| child 15184 | d2c19aea17bc |
--- a/src/HOL/simpdata.ML Fri May 14 16:52:53 2004 +0200 +++ b/src/HOL/simpdata.ML Fri May 14 16:53:15 2004 +0200 @@ -72,7 +72,7 @@ val simp_thms = thms "simp_thms"; val split_if = thm "split_if"; val split_if_asm = thm "split_if_asm"; - +val atomize_not = thm"atomize_not"; local val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R"