--- a/Journal/Paper.thy	Mon Sep 05 20:59:50 2011 +0000
+++ b/Journal/Paper.thy	Tue Sep 06 02:35:10 2011 +0000
@@ -29,6 +29,9 @@
   "_Collect p P"      <= "{p|xs. P}"
   "_CollectIn p A P"  <= "{p : A. P}"
 
+syntax (latex output)
+  "_UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00\<^bsub>_ \<le> _\<^esub>)/ _)" [0, 0, 10] 10)
+
 abbreviation "ZERO \<equiv> Zero"
 abbreviation "ONE \<equiv> One"
 abbreviation "ATOM \<equiv> Atom"
@@ -2463,9 +2466,10 @@
   
   \noindent
   {\bf Acknowledgements:}
-  We are grateful for the comments we received from Larry
-  Paulson, Tobias Nipkow made us aware of the properties in Lemma~\ref{subseqreg}
-  and Tjark Weber helped us with their proofs.
+  We are grateful for the comments we received from Larry Paulson.  Tobias
+  Nipkow made us aware of the properties in Lemma~\ref{subseqreg} and Tjark
+  Weber helped us with their proofs.
+
 
 *}