| author | berghofe | 
| Wed, 15 Mar 2000 23:41:42 +0100 | |
| changeset 8482 | bbc805ebc904 | 
| parent 8481 | 89d498a8d3f6 | 
| child 8483 | b437907f9b26 | 
--- a/src/HOL/Inductive.thy Wed Mar 15 23:40:59 2000 +0100 +++ b/src/HOL/Inductive.thy Wed Mar 15 23:41:42 2000 +0100 @@ -16,6 +16,7 @@ setup InductMethod.setup setup InductivePackage.setup setup DatatypePackage.setup +setup PrimrecPackage.setup theorems [mono] = subset_refl imp_refl disj_mono conj_mono ex_mono all_mono