Rule not_not is now stored in theory (needed by Inductive).
authorberghofe
Tue Oct 05 15:24:58 1999 +0200 (1999-10-05)
changeset 77114dae7a4fceaf
parent 7710 bf8cb3fc5d64
child 7712 c522ec2adc37
Rule not_not is now stored in theory (needed by Inductive).
src/HOL/simpdata.ML
     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