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 "\"} & @{thm (rhs) UP.simps(1)}\\ @{thm (lhs) UP.simps(2)} & @{text "\"} & @{thm (rhs) UP.simps(2)}\\ - @{thm (lhs) UP.simps(3)} & @{text "\"} & @{thm (rhs) UP.simps(3)}\\ + @{thm (lhs) UP.simps(3)} & @{text "\"} &\\ + \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 "\"} & @{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"]} &