Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/IsarRef/Thy/Preface.thy
changeset 48957 c04001b3a753
parent 42915 f35aae36cad0 
--- a/doc-src/IsarRef/Thy/Preface.thy	Tue Aug 28 12:22:10 2012 +0200
+++ b/doc-src/IsarRef/Thy/Preface.thy	Tue Aug 28 12:31:53 2012 +0200
@@ -51,11 +51,10 @@
   \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.
+  Isabelle/HOL are described in \chref{ch:hol}.  Although the main
+  language elements are already provided by the Isabelle/Pure
+  framework, examples given in the generic parts will usually refer to
+  Isabelle/HOL.
 
   \medskip Isar commands may be either \emph{proper} document
   constructors, or \emph{improper commands}.  Some proof methods and
isabelle