| changeset 7710 | bf8cb3fc5d64 |
| parent 7700 | 38b6d2643630 |
| child 8303 | 5e7037409118 |
| 7709:545637744a85 | 7710:bf8cb3fc5d64 |
|---|---|
13 "Tools/primrec_package.ML": |
13 "Tools/primrec_package.ML": |
14 |
14 |
15 setup InductivePackage.setup |
15 setup InductivePackage.setup |
16 setup DatatypePackage.setup |
16 setup DatatypePackage.setup |
17 |
17 |
18 theorems [mono] = |
|
19 subset_refl imp_refl disj_mono conj_mono ex_mono all_mono |
|
20 Collect_mono in_mono vimage_mono |
|
21 imp_conv_disj not_not de_Morgan_disj de_Morgan_conj |
|
22 not_all not_ex |
|
23 Ball_def Bex_def |
|
18 |
24 |
19 end |
25 end |