equal
deleted
inserted
replaced
103 exploited in any way.} |
103 exploited in any way.} |
104 \item [$\TXT~text$] is similar to $\TEXT$, but may appear within proofs. |
104 \item [$\TXT~text$] is similar to $\TEXT$, but may appear within proofs. |
105 \end{description} |
105 \end{description} |
106 |
106 |
107 |
107 |
108 \subsection{Type classes and sorts} |
108 \subsection{Type classes and sorts}\label{sec:classes} |
109 |
109 |
110 \indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort} |
110 \indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort} |
111 \begin{matharray}{rcl} |
111 \begin{matharray}{rcl} |
112 \isarcmd{classes} & : & \isartrans{theory}{theory} \\ |
112 \isarcmd{classes} & : & \isartrans{theory}{theory} \\ |
113 \isarcmd{classrel} & : & \isartrans{theory}{theory} \\ |
113 \isarcmd{classrel} & : & \isartrans{theory}{theory} \\ |
114 \isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\ |
114 \isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\ |
115 \end{matharray} |
115 \end{matharray} |
116 |
116 |
117 \begin{rail} |
117 \begin{rail} |
118 'classes' (name ('<' (nameref ',' +))? comment? +) |
118 'classes' (classdecl +) |
119 ; |
119 ; |
120 'classrel' nameref '<' nameref comment? |
120 'classrel' nameref '<' nameref comment? |
121 ; |
121 ; |
122 'defaultsort' sort comment? |
122 'defaultsort' sort comment? |
123 ; |
123 ; |
251 \isarcmd{theorems} & : & \isartrans{theory}{theory} \\ |
251 \isarcmd{theorems} & : & \isartrans{theory}{theory} \\ |
252 \isarcmd{lemmas} & : & \isartrans{theory}{theory} \\ |
252 \isarcmd{lemmas} & : & \isartrans{theory}{theory} \\ |
253 \end{matharray} |
253 \end{matharray} |
254 |
254 |
255 \begin{rail} |
255 \begin{rail} |
256 'axioms' (name attributes? ':' prop comment? +) |
256 'axioms' (axmdecl prop comment? +) |
257 ; |
257 ; |
258 ('theorems' | 'lemmas') thmdef? thmrefs |
258 ('theorems' | 'lemmas') thmdef? thmrefs |
259 ; |
259 ; |
260 \end{rail} |
260 \end{rail} |
261 |
261 |