equal
deleted
inserted
replaced
8 |
8 |
9 |
9 |
10 chapter {* Recipes *} |
10 chapter {* Recipes *} |
11 |
11 |
12 text {* |
12 text {* |
13 Possible further topics: |
13 Possible topics: |
14 |
14 |
15 \begin{itemize} |
15 \begin{itemize} |
16 \item translations/print translations; |
16 \item translations/print translations; |
17 @{ML "ProofContext.print_syntax"} |
17 @{ML "ProofContext.print_syntax"} |
18 |
18 |
19 \item user space type systems (in the form that already exists) |
19 \item user space type systems (in the form that already exists) |
20 |
20 |
21 \item unification and typing algorithms |
21 \item unification and typing algorithms |
|
22 (@{ML_file "Pure/pattern.ML"} implements HOPU) |
22 |
23 |
23 \item useful datastructures: discrimination nets, association lists |
24 \item useful datastructures: discrimination nets, association lists |
24 \end{itemize} |
25 \end{itemize} |
25 *} |
26 *} |
26 |
27 |