changeset 16009 | a6d480e6c5f0 |
parent 15872 | 8336ff711d80 |
child 16039 | dfe264950511 |
16008:861a255cf1e7 | 16009:a6d480e6c5f0 |
---|---|
31 |
31 |
32 begin |
32 begin |
33 |
33 |
34 text{*Every theory of HOL must be a descendant or ancestor of this one!*} |
34 text{*Every theory of HOL must be a descendant or ancestor of this one!*} |
35 |
35 |
36 setup ResAxioms.setup |
|
36 setup Reconstruction.setup |
37 setup Reconstruction.setup |
37 |
38 |
38 end |
39 end |