# HG changeset patch
# User blanchet
# Date 1405761609 -7200
# Node ID b0d31645f47a50dc8694896076218f6d7afb9d9f
# Parent  e4ddd52e1b96d531b4efeffcdefe14b720c0ec7b
doc fixes (contributed by Christian Sternagel)

diff -r e4ddd52e1b96 -r b0d31645f47a src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Sat Jul 19 11:20:09 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Sat Jul 19 11:20:09 2014 +0200
@@ -90,7 +90,7 @@
 \footnote{However, some of the
 internal constructions and most of the internal proof obligations are skipped
 if the @{text quick_and_dirty} option is enabled.}
-The package is described in number of papers
+The package is described in a number of papers
 \cite{traytel-et-al-2012,blanchette-et-al-wit,blanchette-et-al-2014-impl,panny-et-al-2014}.
 The central notion is that of a \emph{bounded natural functor} (BNF)---a
 well-behaved type constructor for which nested (co)recursion is supported.
@@ -2628,7 +2628,7 @@
 @{command codatatype} definition.
 
 The command is useful to reason abstractly about BNFs. The axioms are safe
-because there exists BNFs of arbitrary large arities. Applications must import
+because there exist BNFs of arbitrary large arities. Applications must import
 the theory @{theory BNF_Axiomatization}, located in the directory
 \verb|~~/src/|\allowbreak\verb|HOL/Library|, to use this functionality.
 *}
diff -r e4ddd52e1b96 -r b0d31645f47a src/Doc/Datatypes/document/root.tex
--- a/src/Doc/Datatypes/document/root.tex	Sat Jul 19 11:20:09 2014 +0200
+++ b/src/Doc/Datatypes/document/root.tex	Sat Jul 19 11:20:09 2014 +0200
@@ -51,6 +51,7 @@
 \renewcommand\isachardoublequoteclose{\/\kern.15ex\mbox{\upshape{''}}}
 \renewcommand\isacharverbatimopen{\isacharbraceleft\isacharasterisk}
 \renewcommand\isacharverbatimclose{\isacharasterisk\isacharbraceright}
+\renewcommand{\isasyminverse}{\isamath{{}^{-}}}
 
 \hyphenation{isa-belle}