doc-src/IsarRef/isar-ref.tex
changeset 7335 abba35b98892
parent 7297 c1eeeadbe80a
child 7466 7df66ce6508a
     1.1 --- a/doc-src/IsarRef/isar-ref.tex	Tue Aug 24 11:54:13 1999 +0200
     1.2 +++ b/doc-src/IsarRef/isar-ref.tex	Tue Aug 24 15:38:18 1999 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4    Isabelle/Isar input may consist either of \emph{proper document
     1.5      constructors}, or \emph{improper auxiliary commands} (for diagnostics,
     1.6    exploration etc.).  Proof texts consisting of proper document constructors
     1.7 -  only admit a purely static reading, thus being intelligible later without
     1.8 +  only, admit a purely static reading, thus being intelligible later without
     1.9    requiring dynamic replay that is so typical for traditional proof scripts.
    1.10    Any of the Isabelle/Isar commands may be executed in single-steps, so
    1.11    basically the interpreter has a proof text debugger already built-in.
    1.12 @@ -63,12 +63,11 @@
    1.13    including forward and backward tracing of partial documents; intermediate
    1.14    states may be inspected by diagnostic commands.
    1.15    
    1.16 -  The Isar subsystem of Isabelle is tightly integrated into the Isabelle/Pure
    1.17 -  meta-logic implementation.  Theories, theorems, proof procedures etc.\ may
    1.18 -  be used interchangeably between Isabelle-classic proof scripts and
    1.19 -  Isabelle/Isar documents.  Isar is as generic as Isabelle, able to support a
    1.20 -  wide range of object-logics.  The current end-user setup is mainly for
    1.21 -  Isabelle/HOL.
    1.22 +  The Isar subsystem is tightly integrated into the Isabelle/Pure meta-logic
    1.23 +  implementation.  Theories, theorems, proof procedures etc.\ may be used
    1.24 +  interchangeably between Isabelle-classic proof scripts and Isabelle/Isar
    1.25 +  documents.  Isar is as generic as Isabelle, able to support a wide range of
    1.26 +  object-logics.  The current end-user setup is mainly for Isabelle/HOL.
    1.27  \end{abstract}
    1.28  
    1.29  \pagenumbering{roman} \tableofcontents \clearfirst