src/HOL/Inductive.thy
changeset 7710 bf8cb3fc5d64
parent 7700 38b6d2643630
child 8303 5e7037409118
     1.1 --- a/src/HOL/Inductive.thy	Tue Oct 05 14:11:34 1999 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Tue Oct 05 15:23:22 1999 +0200
     1.3 @@ -15,5 +15,11 @@
     1.4  setup InductivePackage.setup
     1.5  setup DatatypePackage.setup
     1.6  
     1.7 +theorems [mono] =
     1.8 +   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono
     1.9 +   Collect_mono in_mono vimage_mono
    1.10 +   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    1.11 +   not_all not_ex
    1.12 +   Ball_def Bex_def
    1.13  
    1.14  end