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

doc-src/IsarRef/basics.tex

changeset 7895 | 7c492d8bc8e3 |

parent 7466 | 7df66ce6508a |

child 7981 | 5120a2a15d06 |

1.1 --- a/doc-src/IsarRef/basics.tex Thu Oct 21 15:57:26 1999 +0200 1.2 +++ b/doc-src/IsarRef/basics.tex Thu Oct 21 17:42:21 1999 +0200 1.3 @@ -1,21 +1,22 @@ 1.4 1.5 \chapter{Basic Concepts}\label{ch:basics} 1.6 1.7 +\section{Isabelle/Isar theories} 1.8 + 1.9 Isabelle/Isar offers two main improvements over classic Isabelle: 1.10 \begin{enumerate} 1.11 \item A new \emph{theory format}, occasionally referred to as ``new-style 1.12 - theories'', supporting interactive development with unlimited undo 1.13 - operation. 1.14 -\item A \emph{formal proof language} designed to support intelligible 1.15 - semi-automated reasoning. Rather than putting together tactic scripts, the 1.16 - author is enabled to express the reasoning in way that is close to 1.17 - mathematical practice. 1.18 + theories'', supporting interactive development and unlimited undo operation. 1.19 +\item A \emph{formal proof document language} designed to support intelligible 1.20 + semi-automated reasoning. Instead of putting together unreadable tactic 1.21 + scripts, the author is enabled to express the reasoning in way that is close 1.22 + to mathematical practice. 1.23 \end{enumerate} 1.24 1.25 The Isar proof language is embedded into the new theory format as a proper 1.26 sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or 1.27 -$\LEMMANAME$ at the theory level, and left with the conclusion of the proof 1.28 -(via $\QEDNAME$ etc.). Some theory extension mechanisms require proof as 1.29 +$\LEMMANAME$ at the theory level, and left again with the final conclusion 1.30 +(e.g.\ via $\QEDNAME$). A few theory extension mechanisms require proof as 1.31 well, such as the HOL $\isarkeyword{typedef}$ which demands non-emptiness of 1.32 the representing sets. 1.33 1.34 @@ -29,10 +30,10 @@ 1.35 1.36 \begin{warn} 1.37 Currently Proof~General does \emph{not} support mixed interactive 1.38 - development of classic Isabelle theory files and tactic scripts together 1.39 + development of classic Isabelle theory files and tactic scripts, together 1.40 with Isar documents at the same time. The ``\texttt{isa}'' and 1.41 ``\texttt{isar}'' versions of Proof~General are handled as two different 1.42 - theorem proving systems, only one may be active at the same time. 1.43 + theorem proving systems, only one of these may be active. 1.44 \end{warn} 1.45 1.46 Porting of existing tactic scripts is best done by running two separate 1.47 @@ -56,7 +57,6 @@ 1.48 1.49 \subsection{Attributes} 1.50 1.51 - 1.52 %%% Local Variables: 1.53 %%% mode: latex 1.54 %%% TeX-master: "isar-ref"