| changeset 8482 | bbc805ebc904 |
| parent 8343 | fb604f0e5640 |
| child 10212 | 33fe2d701ddd |
--- 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