--- a/doc-src/IsarRef/IsaMakefile Thu May 26 22:42:52 2011 +0200
+++ b/doc-src/IsarRef/IsaMakefile Tue May 31 22:15:39 2011 +0200
@@ -23,7 +23,7 @@
$(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/Base.thy \
Thy/First_Order_Logic.thy Thy/Framework.thy Thy/Inner_Syntax.thy \
- Thy/Introduction.thy Thy/Outer_Syntax.thy Thy/Spec.thy Thy/Proof.thy \
+ Thy/Preface.thy Thy/Outer_Syntax.thy Thy/Spec.thy Thy/Proof.thy \
Thy/Misc.thy Thy/Document_Preparation.thy Thy/Generic.thy \
Thy/HOL_Specific.thy Thy/Quick_Reference.thy Thy/Symbols.thy \
Thy/ML_Tactic.thy
--- a/doc-src/IsarRef/Makefile Thu May 26 22:42:52 2011 +0200
+++ b/doc-src/IsarRef/Makefile Tue May 31 22:15:39 2011 +0200
@@ -14,7 +14,7 @@
Thy/document/ML_Tactic.tex Thy/document/Proof.tex \
Thy/document/Quick_Reference.tex Thy/document/Spec.tex \
Thy/document/ZF_Specific.tex Thy/document/Inner_Syntax.tex \
- Thy/document/Introduction.tex Thy/document/Document_Preparation.tex \
+ Thy/document/Preface.tex Thy/document/Document_Preparation.tex \
Thy/document/Misc.tex Thy/document/Outer_Syntax.tex \
Thy/document/Symbols.tex ../isar.sty ../proof.sty ../iman.sty \
../extra.sty ../ttbox.sty ../../lib/texinputs/isabelle.sty \
--- a/doc-src/IsarRef/Thy/Introduction.thy Thu May 26 22:42:52 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,73 +0,0 @@
-theory Introduction
-imports Base Main
-begin
-
-chapter {* Introduction *}
-
-section {* Overview *}
-
-text {*
- The \emph{Isabelle} system essentially provides a generic
- infrastructure for building deductive systems (programmed in
- Standard ML), with a special focus on interactive theorem proving in
- higher-order logics. Many years ago, even end-users would refer to
- certain ML functions (goal commands, tactics, tacticals etc.) to
- pursue their everyday theorem proving tasks.
-
- In contrast \emph{Isar} provides an interpreted language environment
- of its own, which has been specifically tailored for the needs of
- theory and proof development. Compared to raw ML, the Isabelle/Isar
- top-level provides a more robust and comfortable development
- platform, with proper support for theory development graphs, managed
- transactions with unlimited undo etc. The Isabelle/Isar version of
- the \emph{Proof~General} user interface
- \cite{proofgeneral,Aspinall:TACAS:2000} provides a decent front-end
- for interactive theory and proof development in this advanced
- theorem proving environment, even though it is somewhat biased
- towards old-style proof scripts.
-
- \medskip Apart from the technical advances over bare-bones ML
- programming, the main purpose of the Isar language is to provide a
- conceptually different view on machine-checked proofs
- \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. \emph{Isar} stands for
- \emph{Intelligible semi-automated reasoning}. Drawing from both the
- traditions of informal mathematical proof texts and high-level
- programming languages, Isar offers a versatile environment for
- structured formal proof documents. Thus properly written Isar
- proofs become accessible to a broader audience than unstructured
- tactic scripts (which typically only provide operational information
- for the machine). Writing human-readable proof texts certainly
- requires some additional efforts by the writer to achieve a good
- presentation, both of formal and informal parts of the text. On the
- other hand, human-readable formal texts gain some value in their own
- right, independently of the mechanic proof-checking process.
-
- Despite its grand design of structured proof texts, Isar is able to
- assimilate the old tactical style as an ``improper'' sub-language.
- This provides an easy upgrade path for existing tactic scripts, as
- well as some means for interactive experimentation and debugging of
- structured proofs. Isabelle/Isar supports a broad range of proof
- styles, both readable and unreadable ones.
-
- \medskip The generic Isabelle/Isar framework (see
- \chref{ch:isar-framework}) works reasonably well for any Isabelle
- object-logic that conforms to the natural deduction view of the
- Isabelle/Pure framework. Specific language elements introduced by
- the major object-logics are described in \chref{ch:hol}
- (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf}
- (Isabelle/ZF). The main language elements are already provided by
- the Isabelle/Pure framework. Nevertheless, examples given in the
- generic parts will usually refer to Isabelle/HOL as well.
-
- \medskip Isar commands may be either \emph{proper} document
- constructors, or \emph{improper commands}. Some proof methods and
- attributes introduced later are classified as improper as well.
- Improper Isar language elements, which are marked by ``@{text
- "\<^sup>*"}'' in the subsequent chapters; they are often helpful
- when developing proof documents, but their use is discouraged for
- the final human-readable outcome. Typical examples are diagnostic
- commands that print terms or theorems according to the current
- context; other commands emulate old-style tactical theorem proving.
-*}
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/Preface.thy Tue May 31 22:15:39 2011 +0200
@@ -0,0 +1,71 @@
+theory Preface
+imports Base Main
+begin
+
+chapter {* Preface *}
+
+text {*
+ The \emph{Isabelle} system essentially provides a generic
+ infrastructure for building deductive systems (programmed in
+ Standard ML), with a special focus on interactive theorem proving in
+ higher-order logics. Many years ago, even end-users would refer to
+ certain ML functions (goal commands, tactics, tacticals etc.) to
+ pursue their everyday theorem proving tasks.
+
+ In contrast \emph{Isar} provides an interpreted language environment
+ of its own, which has been specifically tailored for the needs of
+ theory and proof development. Compared to raw ML, the Isabelle/Isar
+ top-level provides a more robust and comfortable development
+ platform, with proper support for theory development graphs, managed
+ transactions with unlimited undo etc. The Isabelle/Isar version of
+ the \emph{Proof~General} user interface
+ \cite{proofgeneral,Aspinall:TACAS:2000} provides a decent front-end
+ for interactive theory and proof development in this advanced
+ theorem proving environment, even though it is somewhat biased
+ towards old-style proof scripts.
+
+ \medskip Apart from the technical advances over bare-bones ML
+ programming, the main purpose of the Isar language is to provide a
+ conceptually different view on machine-checked proofs
+ \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. \emph{Isar} stands for
+ \emph{Intelligible semi-automated reasoning}. Drawing from both the
+ traditions of informal mathematical proof texts and high-level
+ programming languages, Isar offers a versatile environment for
+ structured formal proof documents. Thus properly written Isar
+ proofs become accessible to a broader audience than unstructured
+ tactic scripts (which typically only provide operational information
+ for the machine). Writing human-readable proof texts certainly
+ requires some additional efforts by the writer to achieve a good
+ presentation, both of formal and informal parts of the text. On the
+ other hand, human-readable formal texts gain some value in their own
+ right, independently of the mechanic proof-checking process.
+
+ Despite its grand design of structured proof texts, Isar is able to
+ assimilate the old tactical style as an ``improper'' sub-language.
+ This provides an easy upgrade path for existing tactic scripts, as
+ well as some means for interactive experimentation and debugging of
+ structured proofs. Isabelle/Isar supports a broad range of proof
+ styles, both readable and unreadable ones.
+
+ \medskip The generic Isabelle/Isar framework (see
+ \chref{ch:isar-framework}) works reasonably well for any Isabelle
+ object-logic that conforms to the natural deduction view of the
+ Isabelle/Pure framework. Specific language elements introduced by
+ the major object-logics are described in \chref{ch:hol}
+ (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf}
+ (Isabelle/ZF). The main language elements are already provided by
+ the Isabelle/Pure framework. Nevertheless, examples given in the
+ generic parts will usually refer to Isabelle/HOL as well.
+
+ \medskip Isar commands may be either \emph{proper} document
+ constructors, or \emph{improper commands}. Some proof methods and
+ attributes introduced later are classified as improper as well.
+ Improper Isar language elements, which are marked by ``@{text
+ "\<^sup>*"}'' in the subsequent chapters; they are often helpful
+ when developing proof documents, but their use is discouraged for
+ the final human-readable outcome. Typical examples are diagnostic
+ commands that print terms or theorems according to the current
+ context; other commands emulate old-style tactical theorem proving.
+*}
+
+end
--- a/doc-src/IsarRef/Thy/ROOT.ML Thu May 26 22:42:52 2011 +0200
+++ b/doc-src/IsarRef/Thy/ROOT.ML Tue May 31 22:15:39 2011 +0200
@@ -1,7 +1,7 @@
quick_and_dirty := true;
use_thys [
- "Introduction",
+ "Preface",
"Framework",
"First_Order_Logic",
"Outer_Syntax",
--- a/doc-src/IsarRef/Thy/document/Introduction.tex Thu May 26 22:42:52 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Introduction}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Introduction\isanewline
-\isakeyword{imports}\ Base\ Main\isanewline
-\isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupchapter{Introduction%
-}
-\isamarkuptrue%
-%
-\isamarkupsection{Overview%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The \emph{Isabelle} system essentially provides a generic
- infrastructure for building deductive systems (programmed in
- Standard ML), with a special focus on interactive theorem proving in
- higher-order logics. Many years ago, even end-users would refer to
- certain ML functions (goal commands, tactics, tacticals etc.) to
- pursue their everyday theorem proving tasks.
-
- In contrast \emph{Isar} provides an interpreted language environment
- of its own, which has been specifically tailored for the needs of
- theory and proof development. Compared to raw ML, the Isabelle/Isar
- top-level provides a more robust and comfortable development
- platform, with proper support for theory development graphs, managed
- transactions with unlimited undo etc. The Isabelle/Isar version of
- the \emph{Proof~General} user interface
- \cite{proofgeneral,Aspinall:TACAS:2000} provides a decent front-end
- for interactive theory and proof development in this advanced
- theorem proving environment, even though it is somewhat biased
- towards old-style proof scripts.
-
- \medskip Apart from the technical advances over bare-bones ML
- programming, the main purpose of the Isar language is to provide a
- conceptually different view on machine-checked proofs
- \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. \emph{Isar} stands for
- \emph{Intelligible semi-automated reasoning}. Drawing from both the
- traditions of informal mathematical proof texts and high-level
- programming languages, Isar offers a versatile environment for
- structured formal proof documents. Thus properly written Isar
- proofs become accessible to a broader audience than unstructured
- tactic scripts (which typically only provide operational information
- for the machine). Writing human-readable proof texts certainly
- requires some additional efforts by the writer to achieve a good
- presentation, both of formal and informal parts of the text. On the
- other hand, human-readable formal texts gain some value in their own
- right, independently of the mechanic proof-checking process.
-
- Despite its grand design of structured proof texts, Isar is able to
- assimilate the old tactical style as an ``improper'' sub-language.
- This provides an easy upgrade path for existing tactic scripts, as
- well as some means for interactive experimentation and debugging of
- structured proofs. Isabelle/Isar supports a broad range of proof
- styles, both readable and unreadable ones.
-
- \medskip The generic Isabelle/Isar framework (see
- \chref{ch:isar-framework}) works reasonably well for any Isabelle
- object-logic that conforms to the natural deduction view of the
- Isabelle/Pure framework. Specific language elements introduced by
- the major object-logics are described in \chref{ch:hol}
- (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf}
- (Isabelle/ZF). The main language elements are already provided by
- the Isabelle/Pure framework. Nevertheless, examples given in the
- generic parts will usually refer to Isabelle/HOL as well.
-
- \medskip Isar commands may be either \emph{proper} document
- constructors, or \emph{improper commands}. Some proof methods and
- attributes introduced later are classified as improper as well.
- Improper Isar language elements, which are marked by ``\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}'' in the subsequent chapters; they are often helpful
- when developing proof documents, but their use is discouraged for
- the final human-readable outcome. Typical examples are diagnostic
- commands that print terms or theorems according to the current
- context; other commands emulate old-style tactical theorem proving.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/document/Preface.tex Tue May 31 22:15:39 2011 +0200
@@ -0,0 +1,107 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Preface}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Preface\isanewline
+\isakeyword{imports}\ Base\ Main\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Preface%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \emph{Isabelle} system essentially provides a generic
+ infrastructure for building deductive systems (programmed in
+ Standard ML), with a special focus on interactive theorem proving in
+ higher-order logics. Many years ago, even end-users would refer to
+ certain ML functions (goal commands, tactics, tacticals etc.) to
+ pursue their everyday theorem proving tasks.
+
+ In contrast \emph{Isar} provides an interpreted language environment
+ of its own, which has been specifically tailored for the needs of
+ theory and proof development. Compared to raw ML, the Isabelle/Isar
+ top-level provides a more robust and comfortable development
+ platform, with proper support for theory development graphs, managed
+ transactions with unlimited undo etc. The Isabelle/Isar version of
+ the \emph{Proof~General} user interface
+ \cite{proofgeneral,Aspinall:TACAS:2000} provides a decent front-end
+ for interactive theory and proof development in this advanced
+ theorem proving environment, even though it is somewhat biased
+ towards old-style proof scripts.
+
+ \medskip Apart from the technical advances over bare-bones ML
+ programming, the main purpose of the Isar language is to provide a
+ conceptually different view on machine-checked proofs
+ \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. \emph{Isar} stands for
+ \emph{Intelligible semi-automated reasoning}. Drawing from both the
+ traditions of informal mathematical proof texts and high-level
+ programming languages, Isar offers a versatile environment for
+ structured formal proof documents. Thus properly written Isar
+ proofs become accessible to a broader audience than unstructured
+ tactic scripts (which typically only provide operational information
+ for the machine). Writing human-readable proof texts certainly
+ requires some additional efforts by the writer to achieve a good
+ presentation, both of formal and informal parts of the text. On the
+ other hand, human-readable formal texts gain some value in their own
+ right, independently of the mechanic proof-checking process.
+
+ Despite its grand design of structured proof texts, Isar is able to
+ assimilate the old tactical style as an ``improper'' sub-language.
+ This provides an easy upgrade path for existing tactic scripts, as
+ well as some means for interactive experimentation and debugging of
+ structured proofs. Isabelle/Isar supports a broad range of proof
+ styles, both readable and unreadable ones.
+
+ \medskip The generic Isabelle/Isar framework (see
+ \chref{ch:isar-framework}) works reasonably well for any Isabelle
+ object-logic that conforms to the natural deduction view of the
+ Isabelle/Pure framework. Specific language elements introduced by
+ the major object-logics are described in \chref{ch:hol}
+ (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf}
+ (Isabelle/ZF). The main language elements are already provided by
+ the Isabelle/Pure framework. Nevertheless, examples given in the
+ generic parts will usually refer to Isabelle/HOL as well.
+
+ \medskip Isar commands may be either \emph{proper} document
+ constructors, or \emph{improper commands}. Some proof methods and
+ attributes introduced later are classified as improper as well.
+ Improper Isar language elements, which are marked by ``\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}'' in the subsequent chapters; they are often helpful
+ when developing proof documents, but their use is discouraged for
+ the final human-readable outcome. Typical examples are diagnostic
+ commands that print terms or theorems according to the current
+ context; other commands emulate old-style tactical theorem proving.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/doc-src/IsarRef/isar-ref.tex Thu May 26 22:42:52 2011 +0200
+++ b/doc-src/IsarRef/isar-ref.tex Tue May 31 22:15:39 2011 +0200
@@ -46,10 +46,12 @@
\maketitle
-\pagenumbering{roman} \tableofcontents \clearfirst
+\pagenumbering{roman}
+{\def\isamarkupchapter#1{\chapter*{#1}}\input{Thy/document/Preface.tex}}
+\tableofcontents
+\clearfirst
\part{Basic Concepts}
-\input{Thy/document/Introduction.tex}
\input{Thy/document/Framework.tex}
\input{Thy/document/First_Order_Logic.tex}
\part{General Language Elements}