# HG changeset patch # User Christian Urban # Date 1279468985 -3600 # Node ID 43da9adf4759142344781cd82a42f4d5b1677569 # Parent 3aeb58524131f3182f331a328994987daa1de377# Parent d7dfe272b4f84db2dc3122ad06dd9313a2131fff merged diff -r d7dfe272b4f8 -r 43da9adf4759 Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Sun Jul 18 16:06:34 2010 +0100 +++ b/Quotient-Paper/Paper.thy Sun Jul 18 17:03:05 2010 +0100 @@ -821,10 +821,10 @@ package establishes the following three proof steps: \begin{center} - \begin{tabular}{r@ {\hspace{4mm}}l} - 1.) & @{text "raw_thm \ reg_thm"}\\ - 2.) & @{text "reg_thm \ inj_thm"}\\ - 3.) & @{text "inj_thm \ quot_thm"}\\ + \begin{tabular}{l@ {\hspace{4mm}}l} + 1.) Regularisation & @{text "raw_thm \ reg_thm"}\\ + 2.) Injection & @{text "reg_thm \ inj_thm"}\\ + 3.) Cleaning & @{text "inj_thm \ quot_thm"}\\ \end{tabular} \end{center}