equal
deleted
inserted
replaced
23 \item translations/print translations; |
23 \item translations/print translations; |
24 @{ML "ProofContext.print_syntax"} |
24 @{ML "ProofContext.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 unification and typing algorithms |
28 \item useful datastructures: discrimination nets, graphs, association lists |
29 (@{ML_file "Pure/pattern.ML"} implements HOPU) |
|
30 |
|
31 \item useful datastructures: discrimination nets, association lists |
|
32 |
29 |
33 \item Brief history of Isabelle |
30 \item Brief history of Isabelle |
34 \end{itemize} |
31 \end{itemize} |
35 *} |
32 *} |
36 |
33 |