equal
deleted
inserted
replaced
11 text \<open> |
11 text \<open> |
12 Possible topics: |
12 Possible topics: |
13 |
13 |
14 \begin{itemize} |
14 \begin{itemize} |
15 \item translations/print translations; |
15 \item translations/print translations; |
16 @{ML "Proof_Context.print_syntax"} |
16 @{ML \<open>Proof_Context.print_syntax\<close>} |
17 |
17 |
18 \item 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 \item useful datastructures: discrimination nets, graphs, association lists |
20 \item useful datastructures: discrimination nets, graphs, association lists |
21 |
21 |