# HG changeset patch
# User Brian Huffman <brianh@cs.pdx.edu>
# Date 1270711508 25200
# Node ID 176690691b0b091c6e22f6543858d4bac1b29718
# Parent  a862a3befe3745669125ad5f9373bb00b8fc808e
remove extra word

diff -r a862a3befe37 -r 176690691b0b Pearl/Paper.thy
--- a/Pearl/Paper.thy	Thu Apr 08 00:09:53 2010 -0700
+++ b/Pearl/Paper.thy	Thu Apr 08 00:25:08 2010 -0700
@@ -741,7 +741,7 @@
   provided @{thm (prem 1) finite_supp_unique[no_vars]},
   @{thm (prem 2) finite_supp_unique[no_vars]}, and for
   all @{text "a \<in> S"} and all @{text "b \<notin> S"}, with @{text a}
-  and @{text b} having the same sort, then \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}}
+  and @{text b} having the same sort, \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}}
   \end{lemma}
 
   \begin{proof}