equal
deleted
inserted
replaced
19 text {* |
19 text {* |
20 Possible topics: |
20 Possible topics: |
21 |
21 |
22 \begin{itemize} |
22 \begin{itemize} |
23 \item translations/print translations; |
23 \item translations/print translations; |
24 @{ML "ProofContext.print_syntax"} |
24 @{ML "Proof_Context.print_syntax"} |
25 |
25 |
26 \item user space type systems (in the form that already exists) |
26 \item user space type systems (in the form that already exists) |
27 |
27 |
28 \item useful datastructures: discrimination nets, graphs, association lists |
28 \item useful datastructures: discrimination nets, graphs, association lists |
29 |
29 |