equal
deleted
inserted
replaced
408 term & : & \isarantiq \\ |
408 term & : & \isarantiq \\ |
409 typ & : & \isarantiq \\ |
409 typ & : & \isarantiq \\ |
410 text & : & \isarantiq \\ |
410 text & : & \isarantiq \\ |
411 goals & : & \isarantiq \\ |
411 goals & : & \isarantiq \\ |
412 subgoals & : & \isarantiq \\ |
412 subgoals & : & \isarantiq \\ |
|
413 prf & : & \isarantiq \\ |
|
414 full_prf & : & \isarantiq \\ |
413 \end{matharray} |
415 \end{matharray} |
414 |
416 |
415 The text body of formal comments (see also \S\ref{sec:comments}) may contain |
417 The text body of formal comments (see also \S\ref{sec:comments}) may contain |
416 antiquotations of logical entities, such as theorems, terms and types, which |
418 antiquotations of logical entities, such as theorems, terms and types, which |
417 are to be presented in the final output produced by the Isabelle document |
419 are to be presented in the final output produced by the Isabelle document |
438 'prop' options prop | |
440 'prop' options prop | |
439 'term' options term | |
441 'term' options term | |
440 'typ' options type | |
442 'typ' options type | |
441 'text' options name | |
443 'text' options name | |
442 'goals' options | |
444 'goals' options | |
443 'subgoals' options |
445 'subgoals' options | |
|
446 'prf' options thmrefs | |
|
447 'full\_prf' options thmrefs |
444 ; |
448 ; |
445 options: '[' (option * ',') ']' |
449 options: '[' (option * ',') ']' |
446 ; |
450 ; |
447 option: name | name '=' name |
451 option: name | name '=' name |
448 ; |
452 ; |
475 Please do not include goal states into document output unless you really |
479 Please do not include goal states into document output unless you really |
476 know what you are doing! |
480 know what you are doing! |
477 |
481 |
478 \item [$\at\{subgoals\}$] behaves almost like $goals$, except that it does not |
482 \item [$\at\{subgoals\}$] behaves almost like $goals$, except that it does not |
479 print the main goal. |
483 print the main goal. |
|
484 |
|
485 \item [$\at\{prf~\vec a\}$] prints the (compact) proof terms corresponding to |
|
486 the theorems $\vec a$. Note that this |
|
487 requires proof terms to be switched on for the current object logic |
|
488 (see the ``Proof terms'' section of the Isabelle reference manual |
|
489 for information on how to do this). |
|
490 |
|
491 \item [$\at\{full_prf~\vec a\}$] is like $\at\{prf~\vec a\}$, but displays |
|
492 the full proof terms, i.e.\ also displays information omitted in |
|
493 the compact proof term, which is denoted by ``$_$'' placeholders there. |
480 |
494 |
481 \end{descr} |
495 \end{descr} |
482 |
496 |
483 \medskip |
497 \medskip |
484 |
498 |