equal
deleted
inserted
replaced
27 \item[-] sometimes awkward case distinctions, alleviated by operator 'the' |
27 \item[-] sometimes awkward case distinctions, alleviated by operator 'the' |
28 \end{itemize} |
28 \end{itemize} |
29 \end{itemize} |
29 \end{itemize} |
30 *} |
30 *} |
31 |
31 |
32 types ('a, 'b) table --{* table with key type 'a and contents type 'b *} |
32 type_synonym ('a, 'b) table --{* table with key type 'a and contents type 'b *} |
33 = "'a \<rightharpoonup> 'b" |
33 = "'a \<rightharpoonup> 'b" |
34 ('a, 'b) tables --{* non-unique table with key 'a and contents 'b *} |
34 type_synonym ('a, 'b) tables --{* non-unique table with key 'a and contents 'b *} |
35 = "'a \<Rightarrow> 'b set" |
35 = "'a \<Rightarrow> 'b set" |
36 |
36 |
37 |
37 |
38 section "map of / table of" |
38 section "map of / table of" |
39 |
39 |