11 mathematical practice. |
11 mathematical practice. |
12 \end{enumerate} |
12 \end{enumerate} |
13 |
13 |
14 The Isar proof language is embedded into the new theory format as a proper |
14 The Isar proof language is embedded into the new theory format as a proper |
15 sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or |
15 sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or |
16 $\LEMMANAME$ at the theory levels, and left with the final end of proof (e.g.\ |
16 $\LEMMANAME$ at the theory level, and left with the final end of proof (e.g.\ |
17 via $\QEDNAME$). Some theory extension mechanisms require proof as well, such |
17 via $\QEDNAME$). Some theory extension mechanisms require proof as well, such |
18 as the HOL $\isarkeyword{typedef}$ mechanism that only works for non-empty |
18 as the HOL $\isarkeyword{typedef}$ which only works for non-empty representing |
19 representing sets. |
19 sets. |
20 |
20 |
21 New-style theory files may still be associated with an ML file consisting of |
21 New-style theory files may still be associated with an ML file consisting of |
22 plain old tactic scripts. There is no longer any ML binding generated for the |
22 plain old tactic scripts. There is no longer any ML binding generated for the |
23 theory and theorems, though. Functions \texttt{theory}, \texttt{thm}, and |
23 theory and theorems, though. Functions \texttt{theory}, \texttt{thm}, and |
24 \texttt{thms} may be used to retrieve this information from ML (see also |
24 \texttt{thms} may be used to retrieve this information from ML |
25 \cite{isabelle-ref}). Nevertheless, migration between classic Isabelle and |
25 \cite{isabelle-ref}. Nevertheless, migration between classic Isabelle and |
26 Isabelle/Isar is relatively easy. Thus users may start to benefit from |
26 Isabelle/Isar is relatively easy. Thus users may start to benefit from |
27 interactive theory development even before they have any idea of the Isar |
27 interactive theory development even before they have any idea of the Isar |
28 proof language. |
28 proof language. |
29 |
29 |
30 \begin{warn} |
30 \begin{warn} |
31 Proof~General does \emph{not} support mixed interactive development of |
31 Proof~General does \emph{not} support mixed interactive development of |
32 classic Isabelle theory files and tactic scripts together with Isar |
32 classic Isabelle theory files and tactic scripts together with Isar |
33 documents at the same time. The \texttt{isa} and \texttt{isar} versions of |
33 documents at the same time. The ``\texttt{isa}'' and ``\texttt{isar}'' |
34 Proof~General appear as two different theorem proving systems; only one |
34 versions of Proof~General are handled as two different theorem proving |
35 prover may be active at any time. |
35 systems, only one may be active at the same time. |
36 \end{warn} |
36 \end{warn} |
37 |
37 |
38 |
38 |
39 \section{The Isar proof language} |
39 \section{The Isar proof language} |
40 |
40 |
41 This rather important section has not been written yet! Refer to |
41 Sorry, this rather important section has not been written yet! Refer to |
42 \cite{Wenzel:1999:TPHOL} for the time being. |
42 \cite{Wenzel:1999:TPHOL} for the time being. |
43 |
43 |
44 \subsection{Commands} |
44 \subsection{Commands} |
45 |
45 |
46 \subsubsection{Isar primitives} |
46 \subsubsection{Isar primitives} |