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