Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Streamlined setup for monotonicity rules (no longer requires classical rules).
authorberghofe
Fri, 27 Nov 2009 16:26:04 +0100
changeset 33934 25d6a8982e37
parent 33933 e429668becc1
child 33935 b94b4587106a
Streamlined setup for monotonicity rules (no longer requires classical rules).
src/HOL/Inductive.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle