summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/IsarRef/basics.tex

changeset 7315 | 76a39a3784b5 |

parent 7297 | c1eeeadbe80a |

child 7335 | abba35b98892 |

1.1 --- a/doc-src/IsarRef/basics.tex Sun Aug 22 18:21:36 1999 +0200 1.2 +++ b/doc-src/IsarRef/basics.tex Sun Aug 22 21:13:20 1999 +0200 1.3 @@ -4,23 +4,36 @@ 1.4 Isabelle/Isar offers two main improvements over classic Isabelle: 1.5 \begin{enumerate} 1.6 \item A new \emph{theory format}, often referred to as ``new-style theories'', 1.7 - supporting interactive development with unlimited undo operation. 1.8 -\item A formal \emph{proof language} language designed to support 1.9 - \emph{intelligible} semi-automated reasoning. Rather than putting together 1.10 - tactic scripts, the author is enabled to express the reasoning in way that 1.11 - is close to mathematical practice. 1.12 + supporting interactive development and unlimited undo operation. 1.13 +\item A \emph{formal proof language} designed to support intelligible 1.14 + semi-automated reasoning. Rather than putting together tactic scripts, the 1.15 + author is enabled to express the reasoning in way that is close to 1.16 + mathematical practice. 1.17 \end{enumerate} 1.18 1.19 The Isar proof language is embedded into the new theory format as a proper 1.20 sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or 1.21 -$\LEMMANAME$ at the theory levels, and left with the final end of proof. Some 1.22 -theory extension mechanisms require proof as well, such as the HOL 1.23 -$\isarkeyword{typedef}$. 1.24 +$\LEMMANAME$ at the theory levels, and left with the final end of proof (e.g.\ 1.25 +via $\QEDNAME$). Some theory extension mechanisms require proof as well, such 1.26 +as the HOL $\isarkeyword{typedef}$ mechanism that only works for non-empty 1.27 +representing sets. 1.28 1.29 New-style theory files may still be associated with an ML file consisting of 1.30 -plain old tactic scripts. Generally, migration between the two formats is 1.31 -made relatively easy, and users may start to benefit from interactive theory 1.32 -development even before they have any idea of the Isar proof language. 1.33 +plain old tactic scripts. There is no longer any ML binding generated for the 1.34 +theory and theorems, though. Functions \texttt{theory}, \texttt{thm}, and 1.35 +\texttt{thms} may be used to retrieve this information from ML (see also 1.36 +\cite{isabelle-ref}). Nevertheless, migration between classic Isabelle and 1.37 +Isabelle/Isar is relatively easy. Thus users may start to benefit from 1.38 +interactive theory development even before they have any idea of the Isar 1.39 +proof language. 1.40 + 1.41 +\begin{warn} 1.42 + Proof~General does \emph{not} support mixed interactive development of 1.43 + classic Isabelle theory files and tactic scripts together with Isar 1.44 + documents at the same time. The \texttt{isa} and \texttt{isar} versions of 1.45 + Proof~General appear as two different theorem proving systems; only one 1.46 + prover may be active at any time. 1.47 +\end{warn} 1.48 1.49 1.50 \section{The Isar proof language}