equal
deleted
inserted
replaced
521 text {* |
521 text {* |
522 Such bindings are difficult to maintain and can be overwritten by the |
522 Such bindings are difficult to maintain and can be overwritten by the |
523 user accidentally. This often broke Isabelle |
523 user accidentally. This often broke Isabelle |
524 packages. Antiquotations solve this problem, since they are ``linked'' |
524 packages. Antiquotations solve this problem, since they are ``linked'' |
525 statically at compile-time. However, this static linkage also limits their |
525 statically at compile-time. However, this static linkage also limits their |
526 usefulness in cases where data needs to be build up dynamically. In the |
526 usefulness in cases where data needs to be built up dynamically. In the |
527 course of this chapter you will learn more about antiquotations: |
527 course of this chapter you will learn more about antiquotations: |
528 they can simplify Isabelle programming since one can directly access all |
528 they can simplify Isabelle programming since one can directly access all |
529 kinds of logical elements from the ML-level. |
529 kinds of logical elements from the ML-level. |
530 *} |
530 *} |
531 |
531 |
950 |
950 |
951 section {* Theorems *} |
951 section {* Theorems *} |
952 |
952 |
953 text {* |
953 text {* |
954 Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} |
954 Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} |
955 that can only be build by going through interfaces. As a consequence, every proof |
955 that can only be built by going through interfaces. As a consequence, every proof |
956 in Isabelle is correct by construction. This follows the tradition of the LCF approach |
956 in Isabelle is correct by construction. This follows the tradition of the LCF approach |
957 \cite{GordonMilnerWadsworth79}. |
957 \cite{GordonMilnerWadsworth79}. |
958 |
958 |
959 |
959 |
960 To see theorems in ``action'', let us give a proof on the ML-level for the following |
960 To see theorems in ``action'', let us give a proof on the ML-level for the following |