equal
deleted
inserted
replaced
26 specifications within a theory, while @{verbatim "x + y"} without |
26 specifications within a theory, while @{verbatim "x + y"} without |
27 quotes is not. |
27 quotes is not. |
28 |
28 |
29 Printed theory documents usually omit quotes to gain readability |
29 Printed theory documents usually omit quotes to gain readability |
30 (this is a matter of {\LaTeX} macro setup, say via @{verbatim |
30 (this is a matter of {\LaTeX} macro setup, say via @{verbatim |
31 "\\isabellestyle"}, see also @{cite "isabelle-sys"}). Experienced |
31 "\\isabellestyle"}, see also @{cite "isabelle-system"}). Experienced |
32 users of Isabelle/Isar may easily reconstruct the lost technical |
32 users of Isabelle/Isar may easily reconstruct the lost technical |
33 information, while mere readers need not care about quotes at all. |
33 information, while mere readers need not care about quotes at all. |
34 \<close> |
34 \<close> |
35 |
35 |
36 |
36 |