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