# HG changeset patch
# User wenzelm
# Date 1212928246 -7200
# Node ID 66d6da816be70ff6fca3d800a031a64bd481224b
# Parent  3d79bbdaf2ef8aad65c1312d10601c829b8f6280
minor typos;

diff -r 3d79bbdaf2ef -r 66d6da816be7 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Sun Jun 08 14:30:07 2008 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Sun Jun 08 14:30:46 2008 +0200
@@ -408,7 +408,7 @@
   Note the space between \verb!@! and \verb!{! in the tabular argument.
   It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
   as an antiquotation. The styles \verb!lhs! and \verb!rhs!
-  extract the left hand side (or right hand side respectivly) from the
+  extract the left hand side (or right hand side respectively) from the
   conclusion of propositions consisting of a binary operator
   (e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}).
 
diff -r 3d79bbdaf2ef -r 66d6da816be7 doc-src/TutorialI/Protocol/NS_Public.thy
--- a/doc-src/TutorialI/Protocol/NS_Public.thy	Sun Jun 08 14:30:07 2008 +0200
+++ b/doc-src/TutorialI/Protocol/NS_Public.thy	Sun Jun 08 14:30:46 2008 +0200
@@ -310,7 +310,7 @@
 is compromised.
 @{named_thms [display,indent=0,margin=50] analz_Crypt_if [no_vars] (analz_Crypt_if)}
 The simplifier has also used @{text Spy_see_priK}, proved in
-{\S}\ref{sec:regularity}) above, to yield @{term "Ba \<in> bad"}.
+{\S}\ref{sec:regularity} above, to yield @{term "Ba \<in> bad"}.
 
 Recall that this subgoal concerns the case
 where the last message to be sent was
diff -r 3d79bbdaf2ef -r 66d6da816be7 doc-src/TutorialI/Types/numerics.tex
--- a/doc-src/TutorialI/Types/numerics.tex	Sun Jun 08 14:30:07 2008 +0200
+++ b/doc-src/TutorialI/Types/numerics.tex	Sun Jun 08 14:30:46 2008 +0200
@@ -335,7 +335,7 @@
 The real numbers are, moreover, \textbf{complete}: every set of reals that
 is bounded above has a least upper bound.  Completeness distinguishes the
 reals from the rationals, for which the set $\{x\mid x^2<2\}$ has no least
-upper bound.  (It could only be $\surd2$, which is irrational. The
+upper bound.  (It could only be $\surd2$, which is irrational.) The
 formalization of completeness, which is complicated, 
 can be found in theory \texttt{RComplete} of directory
 \texttt{Real}.
@@ -401,7 +401,7 @@
 function, \cdx{abs}. Type \isa{int} is an ordered ring.
 \item 
 \tcdx{field} and \tcdx{ordered_field}: a field extends a ring with the
-multiplicative inverse (called simply \cdx{inverse} and division~(\isa{/}).
+multiplicative inverse (called simply \cdx{inverse} and division~(\isa{/})).
 An ordered field is based on an ordered ring. Type \isa{complex} is a field, while type \isa{real} is an ordered field.
 \item 
 \tcdx{division_by_zero} includes all types where \isa{inverse 0 = 0}