src/HOL/Inductive.thy
changeset 61337 4645502c3c64
parent 61076 bdc1e2f0a86a
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Inductive.thy	Tue Oct 06 13:31:44 2015 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Tue Oct 06 15:14:28 2015 +0200
     1.3 @@ -343,13 +343,13 @@
     1.4  
     1.5  text \<open>Package setup.\<close>
     1.6  
     1.7 -theorems basic_monos =
     1.8 +lemmas basic_monos =
     1.9    subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
    1.10    Collect_mono in_mono vimage_mono
    1.11  
    1.12  ML_file "Tools/inductive.ML"
    1.13  
    1.14 -theorems [mono] =
    1.15 +lemmas [mono] =
    1.16    imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
    1.17    imp_mono not_mono
    1.18    Ball_def Bex_def