equal
deleted
inserted
replaced
56 |
56 |
57 section {* Markup commands \label{sec:markup} *} |
57 section {* Markup commands \label{sec:markup} *} |
58 |
58 |
59 text {* |
59 text {* |
60 \begin{matharray}{rcl} |
60 \begin{matharray}{rcl} |
|
61 @{command_def "header"} & : & \isarkeep{toplevel} \\[0.5ex] |
61 @{command_def "chapter"} & : & \isarkeep{local{\dsh}theory} \\ |
62 @{command_def "chapter"} & : & \isarkeep{local{\dsh}theory} \\ |
62 @{command_def "section"} & : & \isarkeep{local{\dsh}theory} \\ |
63 @{command_def "section"} & : & \isarkeep{local{\dsh}theory} \\ |
63 @{command_def "subsection"} & : & \isarkeep{local{\dsh}theory} \\ |
64 @{command_def "subsection"} & : & \isarkeep{local{\dsh}theory} \\ |
64 @{command_def "subsubsection"} & : & \isarkeep{local{\dsh}theory} \\ |
65 @{command_def "subsubsection"} & : & \isarkeep{local{\dsh}theory} \\ |
65 @{command_def "text"} & : & \isarkeep{local{\dsh}theory} \\ |
66 @{command_def "text"} & : & \isarkeep{local{\dsh}theory} \\ |
77 information on Isabelle's document preparation tools). |
78 information on Isabelle's document preparation tools). |
78 |
79 |
79 \begin{rail} |
80 \begin{rail} |
80 ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text |
81 ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text |
81 ; |
82 ; |
82 ('text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text |
83 ('header' | 'text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text |
83 ; |
84 ; |
84 \end{rail} |
85 \end{rail} |
85 |
86 |
86 \begin{descr} |
87 \begin{descr} |
87 |
88 |
|
89 \item [@{command "header"}~@{text "text"}] provides plain text |
|
90 markup just preceding the formal beginning of a theory. In actual |
|
91 document preparation the corresponding {\LaTeX} macro @{verbatim |
|
92 "\\isamarkupheader"} may be redefined to produce chapter or section |
|
93 headings. See also \secref{sec:markup} for further markup commands. |
|
94 |
88 \item [@{command "chapter"}, @{command "section"}, @{command |
95 \item [@{command "chapter"}, @{command "section"}, @{command |
89 "subsection"}, and @{command "subsubsection"}] mark chapter and |
96 "subsection"}, and @{command "subsubsection"}] mark chapter and |
90 section headings. |
97 section headings. |
91 |
98 |
92 \item [@{command "text"} and @{command "txt"}] specify paragraphs of |
99 \item [@{command "text"} and @{command "txt"}] specify paragraphs of |