# HG changeset patch # User wenzelm # Date 1306872939 -7200 # Node ID f35aae36cad0e87c743c702ae4bcfce830ede4fa # Parent e6ed6b951201ab87749d80401ebc75c71e60076a turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex); diff -r e6ed6b951201 -r f35aae36cad0 doc-src/IsarRef/IsaMakefile --- 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 diff -r e6ed6b951201 -r f35aae36cad0 doc-src/IsarRef/Makefile --- 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 \ diff -r e6ed6b951201 -r f35aae36cad0 doc-src/IsarRef/Thy/Introduction.thy --- 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 diff -r e6ed6b951201 -r f35aae36cad0 doc-src/IsarRef/Thy/Preface.thy --- /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 diff -r e6ed6b951201 -r f35aae36cad0 doc-src/IsarRef/Thy/ROOT.ML --- 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", diff -r e6ed6b951201 -r f35aae36cad0 doc-src/IsarRef/Thy/document/Introduction.tex --- 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: diff -r e6ed6b951201 -r f35aae36cad0 doc-src/IsarRef/Thy/document/Preface.tex --- /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: diff -r e6ed6b951201 -r f35aae36cad0 doc-src/IsarRef/isar-ref.tex --- 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}