src/HOL/Inductive.thy
changeset 58815 fd3f893a40ea
parent 58306 117ba6cbe414
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Inductive.thy	Wed Oct 29 11:33:29 2014 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Wed Oct 29 11:41:54 2014 +0100
     1.3 @@ -258,7 +258,6 @@
     1.4    Collect_mono in_mono vimage_mono
     1.5  
     1.6  ML_file "Tools/inductive.ML"
     1.7 -setup Inductive.setup
     1.8  
     1.9  theorems [mono] =
    1.10    imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj