diff -r 4abb95a7264b -r 014a4ef807dc Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Apr 01 11:34:43 2010 +0200
+++ b/Paper/Paper.thy	Thu Apr 01 12:13:25 2010 +0200
@@ -1655,9 +1655,45 @@
   \end{eqnarray}
 
   With the Property~\ref{avoiding} we can prove a strong induction principle
-  which we show again only for the Core Haskell example:
+  which we show again only for the interesting constructors in the Core Haskell
+  example. We first show the weak induction principle for comparison:
+
+\begin{equation}\nonumber
+\infer
+{
+  @{text "P1 tkind \<and> P2 ckind \<and> \<dots> \<and> P12 cvars"}
+}{
+  \begin{tabular}{cp{7cm}}
+  @{text "P1 KStar"}\\
+  @{text "\<And>tk1 tk2. \<lbrakk>P1 tk1; P1 tk2\<rbrakk> \<Longrightarrow> P1 (KFun tk1 tk2)"}\\
+  @{text "\<dots>"}\\
+  @{text "\<And>v ty t1 t2. \<lbrakk>P3 ty; P7 t1; P7 t2\<rbrakk> \<Longrightarrow> P7 (Let v ty t1 t2)"}\\
+  @{text "\<And>p t al. \<lbrakk>P9 p; P7 t; P8 al\<rbrakk> \<Longrightarrow> P8 (ACons p t al)"}\\
+  @{text "\<dots>"}
+  \end{tabular}
+}
+\end{equation}
+
 
-  
+In comparison, the cases for the same constructors in the derived strong
+induction principle are:
+
+\begin{equation}\nonumber
+\infer
+{
+  @{text "P1 a tkind \<and> P2 a ckind \<and> \<dots> \<and> P12 a cvars"}
+}{
+  \begin{tabular}{cp{7cm}}
+  @{text "\<And>b. P1 b KStar"}\\
+  @{text "\<And>tk1 tk2 b. \<lbrakk>\<And>c. P1 c tk1; \<And>c. P1 c tk2\<rbrakk> \<Longrightarrow> P1 b (KFun tk1 tk2)"}\\
+  @{text "\<dots>"}\\
+  @{text "\<And>v ty t1 t2 b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c t1; \<And>c. P7 c t2; atom var \<sharp> b\<rbrakk> \<Longrightarrow> P7 b (Let v ty t1 t2)"}\\
+  @{text "\<And>p t al b. \<lbrakk>\<And>c. P9 c p; \<And>c. P7 c t; \<And>c. P8 c al; set (bv p) \<sharp>* b\<rbrakk> \<Longrightarrow> P8 b (ACons p t al)"}\\
+  @{text "\<dots>"}
+  \end{tabular}
+}
+\end{equation}
+
 
 *}