38 @{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
38 @{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
39 @{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
39 @{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
40 @{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
40 @{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
41 @{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
41 @{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
42 @{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
42 @{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
43 @{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ |
43 @{command_def "print_state"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ |
44 \end{matharray} |
44 \end{matharray} |
45 |
45 |
46 These diagnostic commands assist interactive development by printing |
46 These diagnostic commands assist interactive development by printing |
47 internal logical entities in a human-readable fashion. |
47 internal logical entities in a human-readable fashion. |
48 |
48 |
97 \item @{command "full_prf"} is like @{command "prf"}, but displays |
97 \item @{command "full_prf"} is like @{command "prf"}, but displays |
98 the full proof term, i.e.\ also displays information omitted in the |
98 the full proof term, i.e.\ also displays information omitted in the |
99 compact proof term, which is denoted by ``@{text _}'' placeholders |
99 compact proof term, which is denoted by ``@{text _}'' placeholders |
100 there. |
100 there. |
101 |
101 |
102 \item @{command "pr"}~@{text "goals"} prints the current proof state |
102 \item @{command "print_state"} prints the current proof state (if |
103 (if present), including current facts and goals. The optional limit |
103 present), including current facts and goals. |
104 arguments affect the number of goals to be displayed, which is |
|
105 initially 10. Omitting limit value leaves the current setting |
|
106 unchanged. |
|
107 |
104 |
108 \end{description} |
105 \end{description} |
109 |
106 |
110 All of the diagnostic commands above admit a list of @{text modes} |
107 All of the diagnostic commands above admit a list of @{text modes} |
111 to be specified, which is appended to the current print mode; see |
108 to be specified, which is appended to the current print mode; see |
112 also \secref{sec:print-modes}. Thus the output behavior may be |
109 also \secref{sec:print-modes}. Thus the output behavior may be |
113 modified according particular print mode features. For example, |
110 modified according particular print mode features. For example, |
114 @{command "pr"}~@{text "(latex xsymbols)"} would print the current |
111 @{command "print_state"}~@{text "(latex xsymbols)"} prints the |
115 proof state with mathematical symbols and special characters |
112 current proof state with mathematical symbols and special characters |
116 represented in {\LaTeX} source, according to the Isabelle style |
113 represented in {\LaTeX} source, according to the Isabelle style |
117 \cite{isabelle-sys}. |
114 \cite{isabelle-sys}. |
118 |
115 |
119 Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more |
116 Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more |
120 systematic way to include formal items into the printed text |
117 systematic way to include formal items into the printed text |