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