equal
deleted
inserted
replaced
1 theory General |
1 theory General |
2 imports Base FirstSteps |
2 imports Base FirstSteps |
3 begin |
3 begin |
4 |
4 |
5 chapter {* General Infrastructure *} |
5 chapter {* General Infrastructure *} |
|
6 |
|
7 text {* |
|
8 Isabelle is build around a few central ideas. One is the LCF-approach to |
|
9 theorem proving where there is a small trusted core and everything else is |
|
10 build on top of this trusted core. |
|
11 |
|
12 *} |
|
13 |
6 |
14 |
7 section {* Terms and Types *} |
15 section {* Terms and Types *} |
8 |
16 |
9 text {* |
17 text {* |
10 One way to construct Isabelle terms, is by using the antiquotation |
18 One way to construct Isabelle terms, is by using the antiquotation |
1640 |
1648 |
1641 section {* Misc (TBD) *} |
1649 section {* Misc (TBD) *} |
1642 |
1650 |
1643 ML {*Datatype.get_info @{theory} "List.list"*} |
1651 ML {*Datatype.get_info @{theory} "List.list"*} |
1644 |
1652 |
|
1653 text {* |
|
1654 FIXME: association lists: |
|
1655 @{ML_file "Pure/General/alist.ML"} |
|
1656 |
|
1657 FIXME: calling the ML-compiler |
|
1658 |
|
1659 *} |
|
1660 |
|
1661 |
|
1662 |
1645 section {* Name Space Issues (TBD) *} |
1663 section {* Name Space Issues (TBD) *} |
1646 |
1664 |
1647 |
1665 |
1648 end |
1666 end |