equal
deleted
inserted
replaced
134 any type variables input without sort constraints. Typically, the default |
134 any type variables input without sort constraints. Typically, the default |
135 sort would be only changed when defining new logics. |
135 sort would be only changed when defining new logics. |
136 \end{description} |
136 \end{description} |
137 |
137 |
138 |
138 |
139 \subsection{Types} |
139 \subsection{Types}\label{sec:types-pure} |
140 |
140 |
141 \indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities} |
141 \indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities} |
142 \begin{matharray}{rcl} |
142 \begin{matharray}{rcl} |
143 \isarcmd{types} & : & \isartrans{theory}{theory} \\ |
143 \isarcmd{types} & : & \isartrans{theory}{theory} \\ |
144 \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\ |
144 \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\ |
325 \end{description} |
325 \end{description} |
326 |
326 |
327 |
327 |
328 \subsection{ML translation functions} |
328 \subsection{ML translation functions} |
329 |
329 |
330 \indexisarcmd{parse_ast_translation}\indexisarcmd{parse_translation} |
330 \indexisarcmd{parse\_ast\_translation}\indexisarcmd{parse\_translation} |
331 \indexisarcmd{print_translation}\indexisarcmd{typed_print_translation} |
331 \indexisarcmd{print\_translation}\indexisarcmd{typed\_print\_translation} |
332 \indexisarcmd{print_ast_translation}\indexisarcmd{token_translation} |
332 \indexisarcmd{print\_ast\_translation}\indexisarcmd{token\_translation} |
333 \begin{matharray}{rcl} |
333 \begin{matharray}{rcl} |
334 \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\ |
334 \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\ |
335 \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\ |
335 \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\ |
336 \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\ |
336 \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\ |
337 \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\ |
337 \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\ |
365 |
365 |
366 \section{Proof commands} |
366 \section{Proof commands} |
367 |
367 |
368 \subsection{Goal statements} |
368 \subsection{Goal statements} |
369 |
369 |
370 \indexisarcmd{} |
370 \indexisarcmd{theorem}\indexisarcmd{lemma} |
|
371 \indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus} |
371 \begin{matharray}{rcl} |
372 \begin{matharray}{rcl} |
372 \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\ |
373 \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\ |
373 \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\ |
374 \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\ |
374 \isarcmd{have} & : & \isartrans{proof(state)}{proof(prove)} \\ |
375 \isarcmd{have} & : & \isartrans{proof(state)}{proof(prove)} \\ |
375 \isarcmd{show} & : & \isartrans{proof(state)}{proof(prove)} \\ |
376 \isarcmd{show} & : & \isartrans{proof(state)}{proof(prove)} \\ |
493 \isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\ |
494 \isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\ |
494 \isarcmd{\{\{} & : & \isartrans{proof(state)}{proof(state)} \\ |
495 \isarcmd{\{\{} & : & \isartrans{proof(state)}{proof(state)} \\ |
495 \isarcmd{\}\}} & : & \isartrans{proof(state)}{proof(state)} \\ |
496 \isarcmd{\}\}} & : & \isartrans{proof(state)}{proof(state)} \\ |
496 \end{matharray} |
497 \end{matharray} |
497 |
498 |
498 \begin{rail} |
|
499 llbrace |
|
500 ; |
|
501 rrbrace |
|
502 ; |
|
503 'next' |
|
504 ; |
|
505 \end{rail} |
|
506 |
|
507 \begin{description} |
499 \begin{description} |
508 \item [$ $] FIXME |
500 \item [$ $] FIXME |
509 \end{description} |
501 \end{description} |
510 |
502 |
511 |
503 |
531 |
523 |
532 |
524 |
533 |
525 |
534 \subsection{Improper proof steps} |
526 \subsection{Improper proof steps} |
535 |
527 |
536 \indexisarcmd{apply}\indexisarcmd{then_apply}\indexisarcmd{back} |
528 \indexisarcmd{apply}\indexisarcmd{then\_apply}\indexisarcmd{back} |
537 \begin{matharray}{rcl} |
529 \begin{matharray}{rcl} |
538 \isarcmd{apply}^* & : & \isartrans{proof}{proof} \\ |
530 \isarcmd{apply}^* & : & \isartrans{proof}{proof} \\ |
539 \isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\ |
531 \isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\ |
540 \isarcmd{back}^* & : & \isartrans{proof}{proof} \\ |
532 \isarcmd{back}^* & : & \isartrans{proof}{proof} \\ |
541 \end{matharray} |
533 \end{matharray} |
591 \end{description} |
583 \end{description} |
592 |
584 |
593 |
585 |
594 \subsection{System operations} |
586 \subsection{System operations} |
595 |
587 |
596 \indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use_thy}\indexisarcmd{use_thy_only} |
588 \indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use\_thy}\indexisarcmd{use\_thy\_only} |
597 \indexisarcmd{update_thy}\indexisarcmd{update_thy_only} |
589 \indexisarcmd{update\_thy}\indexisarcmd{update\_thy\_only} |
598 \begin{matharray}{rcl} |
590 \begin{matharray}{rcl} |
599 \isarcmd{cd} & : & \isarkeep{\cdot} \\ |
591 \isarcmd{cd} & : & \isarkeep{\cdot} \\ |
600 \isarcmd{pwd} & : & \isarkeep{\cdot} \\ |
592 \isarcmd{pwd} & : & \isarkeep{\cdot} \\ |
601 \isarcmd{use_thy} & : & \isarkeep{\cdot} \\ |
593 \isarcmd{use_thy} & : & \isarkeep{\cdot} \\ |
602 \isarcmd{use_thy_only} & : & \isarkeep{\cdot} \\ |
594 \isarcmd{use_thy_only} & : & \isarkeep{\cdot} \\ |