src/HOL/simpdata.ML
changeset 7711 4dae7a4fceaf
parent 7648 8258b93cdd32
child 8114 09a7a180cc99
     1.1 --- a/src/HOL/simpdata.ML	Tue Oct 05 15:23:22 1999 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Tue Oct 05 15:24:58 1999 +0200
     1.3 @@ -194,7 +194,7 @@
     1.4  
     1.5  bind_thms ("ex_simps", ex_simps);
     1.6  bind_thms ("all_simps", all_simps);
     1.7 -
     1.8 +bind_thm ("not_not", not_not);
     1.9  
    1.10  (* Elimination of True from asumptions: *)
    1.11