summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/IsarRef/basics.tex

changeset 7981 | 5120a2a15d06 |

parent 7895 | 7c492d8bc8e3 |

--- a/doc-src/IsarRef/basics.tex Sat Oct 30 20:12:23 1999 +0200 +++ b/doc-src/IsarRef/basics.tex Sat Oct 30 20:13:16 1999 +0200 @@ -1,61 +1,7 @@ -\chapter{Basic Concepts}\label{ch:basics} - -\section{Isabelle/Isar theories} - -Isabelle/Isar offers two main improvements over classic Isabelle: -\begin{enumerate} -\item A new \emph{theory format}, occasionally referred to as ``new-style - theories'', supporting interactive development and unlimited undo operation. -\item A \emph{formal proof document language} designed to support intelligible - semi-automated reasoning. Instead of putting together unreadable tactic - scripts, the author is enabled to express the reasoning in way that is close - to mathematical practice. -\end{enumerate} - -The Isar proof language is embedded into the new theory format as a proper -sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or -$\LEMMANAME$ at the theory level, and left again with the final conclusion -(e.g.\ via $\QEDNAME$). A few theory extension mechanisms require proof as -well, such as the HOL $\isarkeyword{typedef}$ which demands non-emptiness of -the representing sets. - -New-style theory files may still be associated with an ML file consisting of -plain old tactic scripts. There is no longer any ML binding generated for the -theory and theorems, though. ML functions \texttt{theory}, \texttt{thm}, and -\texttt{thms} retrieve this information \cite{isabelle-ref}. Nevertheless, -migration between classic Isabelle and Isabelle/Isar is relatively easy. Thus -users may start to benefit from interactive theory development even before -they have any idea of the Isar proof language. - -\begin{warn} - Currently Proof~General does \emph{not} support mixed interactive - development of classic Isabelle theory files and tactic scripts, together - with Isar documents at the same time. The ``\texttt{isa}'' and - ``\texttt{isar}'' versions of Proof~General are handled as two different - theorem proving systems, only one of these may be active. -\end{warn} - -Porting of existing tactic scripts is best done by running two separate -Proof~General sessions, one for replaying the old script and the other for the -emerging Isabelle/Isar document. - - -\section{The Isar proof language} - -Sorry, this important section has not been written yet! Refer to -\cite{Wenzel:1999:TPHOL} for the time being. - -\subsection{Commands} - -\subsubsection{Isar primitives} - -\subsubsection{Derived elements} - - -\subsection{Methods} - -\subsection{Attributes} +%FIXME +%\chapter{Basic Concepts}\label{ch:basics} +%\section{The Isar proof language} %%% Local Variables: %%% mode: latex