# HG changeset patch
# User urbanc
# Date 1315230241 0
# Node ID a6513d0b16fccd73eed9d017240031ef94f33f97
# Parent  e02155fe8136511aaa0522c3a8cf23c0ef49fd55
slight polishing to SUBSEQ

diff -r e02155fe8136 -r a6513d0b16fc Journal/Paper.thy
--- a/Journal/Paper.thy	Mon Sep 05 13:43:12 2011 +0000
+++ b/Journal/Paper.thy	Mon Sep 05 13:44:01 2011 +0000
@@ -2183,7 +2183,8 @@
   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
   @{thm (lhs) UP.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(1)}\\  
   @{thm (lhs) UP.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(2)}\\ 
-  @{thm (lhs) UP.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(3)}\\ 
+  @{thm (lhs) UP.simps(3)} & @{text "\<equiv>"} &\\ 
+   \multicolumn{3}{r}{@{thm (rhs) UP.simps(3)}}\\ 
   @{thm (lhs) UP.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & 
      @{text "\<equiv>"} & @{thm (rhs) UP.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
   @{thm (lhs) UP.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} &