equal
deleted
inserted
replaced
55 requirements of prover time and GUI space. |
55 requirements of prover time and GUI space. |
56 |
56 |
57 |
57 |
58 *** Document preparation *** |
58 *** Document preparation *** |
59 |
59 |
60 * Isabelle control symbols for markup and formatting: |
60 * Commands 'paragraph' and 'subparagraph' provide additional section |
|
61 headings. Thus there are 6 levels of standard headings, as in HTML. |
|
62 |
|
63 * Text is structured in paragraphs and nested lists, using notation that |
|
64 is similar to Markdown. The control symbols for list items are as |
|
65 follows: |
|
66 |
|
67 \<^item> itemize |
|
68 \<^enum> enumerate |
|
69 \<^descr> description |
|
70 |
|
71 * Text may contain control symbols for markup and formatting as follows: |
61 |
72 |
62 \<^noindent> \noindent |
73 \<^noindent> \noindent |
63 \<^smallskip> \smallskip |
74 \<^smallskip> \smallskip |
64 \<^medskip> \medskip |
75 \<^medskip> \medskip |
65 \<^bigskip> \bigskip |
76 \<^bigskip> \bigskip |
66 |
77 |
67 * Paragraphs and nested lists may be specified similarly to Markdown, |
78 * Command 'text_raw' has been clarified: input text is processed as in |
68 with control symbols to indicate list items as follows: |
79 'text' (with antiquotations and control symbols). The key difference is |
69 |
80 the lack of the surrounding isabelle markup environment in output. |
70 \<^item> itemize |
|
71 \<^enum> enumerate |
|
72 \<^descr> description |
|
73 |
81 |
74 |
82 |
75 *** Isar *** |
83 *** Isar *** |
76 |
84 |
77 * Command 'obtain' binds term abbreviations (via 'is' patterns) in the |
85 * Command 'obtain' binds term abbreviations (via 'is' patterns) in the |