# HG changeset patch
# User berghofe
# Date 1259335564 -3600
# Node ID 25d6a8982e37c11ffd142dda6941aa6211239bdc
# Parent  e429668becc16d88d8025e144505eb776ca991a3
Streamlined setup for monotonicity rules (no longer requires classical rules).

diff -r e429668becc1 -r 25d6a8982e37 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Fri Nov 27 16:24:31 2009 +0100
+++ b/src/HOL/Inductive.thy	Fri Nov 27 16:26:04 2009 +0100
@@ -262,18 +262,13 @@
 theorems basic_monos =
   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
   Collect_mono in_mono vimage_mono
-  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
-  not_all not_ex
-  Ball_def Bex_def
-  induct_rulify_fallback
 
 use "Tools/inductive.ML"
 setup Inductive.setup
 
 theorems [mono] =
   imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
-  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
-  not_all not_ex
+  imp_mono not_mono
   Ball_def Bex_def
   induct_rulify_fallback