doc-src/IsarRef/isar-ref.tex
changeset 7895 7c492d8bc8e3
parent 7836 7a9270282fd3
child 7974 34245feb6e82
     1.1 --- a/doc-src/IsarRef/isar-ref.tex	Thu Oct 21 15:57:26 1999 +0200
     1.2 +++ b/doc-src/IsarRef/isar-ref.tex	Thu Oct 21 17:42:21 1999 +0200
     1.3 @@ -20,6 +20,9 @@
     1.4  \railalias{prop}{\railqtoken{prop}}
     1.5  \railalias{atom}{\railqtoken{atom}}
     1.6  
     1.7 +\newcommand{\drv}{\mathrel{\vdash}}
     1.8 +\newcommand{\edrv}{\mathop{\drv}\nolimits}
     1.9 +
    1.10  
    1.11  \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    1.12  
    1.13 @@ -29,6 +32,9 @@
    1.14  
    1.15  \renewcommand{\phi}{\varphi}
    1.16  
    1.17 +%\includeonly{pure}
    1.18 +
    1.19 +
    1.20  
    1.21  \begin{document}
    1.22  
    1.23 @@ -46,15 +52,15 @@
    1.24    immediately ``executable'', by virtue of the \emph{Isar/VM} interpreter.
    1.25    
    1.26    The current version of Isabelle offers Isar as an alternative proof language
    1.27 -  interface layer, beyond traditional tactic scripts.  The Isabelle/Isar
    1.28 -  system provides an interpreter for the Isar formal proof document language.
    1.29 -  Isabelle/Isar input may consist either of \emph{proper document
    1.30 -    constructors}, or \emph{improper auxiliary commands} (for diagnostics,
    1.31 -  exploration etc.).  Proof texts consisting of proper document constructors
    1.32 -  only, admit a purely static reading, thus being intelligible later without
    1.33 -  requiring dynamic replay that is so typical for traditional proof scripts.
    1.34 -  Any of the Isabelle/Isar commands may be executed in single-steps, so
    1.35 -  basically the interpreter has a proof text debugger already built-in.
    1.36 +  interface layer.  The Isabelle/Isar system provides an interpreter for the
    1.37 +  Isar formal proof document language.  The input may consist either of
    1.38 +  \emph{proper document constructors}, or \emph{improper auxiliary commands}
    1.39 +  (for diagnostics, exploration etc.).  Proof texts consisting of proper
    1.40 +  document constructors only, admit a purely static reading, thus being
    1.41 +  intelligible later without requiring dynamic replay that is so typical for
    1.42 +  traditional proof scripts.  Any of the Isabelle/Isar commands may be
    1.43 +  executed in single-steps, so basically the interpreter has a proof text
    1.44 +  debugger already built-in.
    1.45    
    1.46    Employing the Isar instantiation of \emph{Proof~General}, the generic Emacs
    1.47    interface for interactive proof assistants of LFCS Edinburgh, we arrive at a
    1.48 @@ -65,10 +71,10 @@
    1.49    
    1.50    The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic
    1.51    implementation.  Theories, theorems, proof procedures etc.\ may be used
    1.52 -  interchangeably between Isabelle-classic proof scripts and Isabelle/Isar
    1.53 +  interchangeably between classic Isabelle proof scripts and Isabelle/Isar
    1.54    documents.  Isar is as generic as Isabelle, able to support a wide range of
    1.55 -  object-logics.  The current working environment for end-users is setup
    1.56 -  mainly for Isabelle/HOL.
    1.57 +  object-logics.  Currently, the end-user working environment is most complete
    1.58 +  for Isabelle/HOL.
    1.59  \end{abstract}
    1.60  
    1.61  \pagenumbering{roman} \tableofcontents \clearfirst
    1.62 @@ -89,6 +95,9 @@
    1.63  \include{generic}
    1.64  \include{hol}
    1.65  
    1.66 +\appendix
    1.67 +\include{refcard}
    1.68 +
    1.69  \begingroup
    1.70    \bibliographystyle{plain} \small\raggedright\frenchspacing
    1.71    \bibliography{../manual}