# HG changeset patch
# User huffman
# Date 1323637042 -3600
# Node ID a644ba1d7cf9d247a4a4db569410f57375b8d2f9
# Parent  5edf7a15ff8e60dfe5ecf1391240bbde22e79b80
fix spelling

diff -r 5edf7a15ff8e -r a644ba1d7cf9 doc-src/IsarRef/Thy/Synopsis.thy
--- a/doc-src/IsarRef/Thy/Synopsis.thy	Sun Dec 11 21:54:20 2011 +0100
+++ b/doc-src/IsarRef/Thy/Synopsis.thy	Sun Dec 11 21:57:22 2011 +0100
@@ -302,7 +302,7 @@
 
   have "a < b" sorry
   also
-  have "b\<le> c" sorry
+  have "b \<le> c" sorry
   also
   have "c = d" sorry
   finally
@@ -318,7 +318,7 @@
   \item The notion of @{text trans} rule is very general due to the
   flexibility of Isabelle/Pure rule composition.
 
-  \item User applications may declare there own rules, with some care
+  \item User applications may declare their own rules, with some care
   about the operational details of higher-order unification.
 
   \end{itemize}