# HG changeset patch
# User berghofe
# Date 939129898 -7200
# Node ID 4dae7a4fceaf3ed0c1eb3995766f544897a79a14
# Parent  bf8cb3fc5d64c3a6d697b1ef5f35279160bb1c0c
Rule not_not is now stored in theory (needed by Inductive).

diff -r bf8cb3fc5d64 -r 4dae7a4fceaf src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Oct 05 15:23:22 1999 +0200
+++ b/src/HOL/simpdata.ML	Tue Oct 05 15:24:58 1999 +0200
@@ -194,7 +194,7 @@
 
 bind_thms ("ex_simps", ex_simps);
 bind_thms ("all_simps", all_simps);
-
+bind_thm ("not_not", not_not);
 
 (* Elimination of True from asumptions: *)