--- a/src/HOL/Lambda/Commutation.thy Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/Commutation.thy Wed Nov 23 22:26:13 2005 +0100
@@ -197,11 +197,11 @@
\<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
\<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
-using wf
+ using wf
proof induct
case (less x b c)
- have IH: "\<And>y b c. \<lbrakk>(y,x) \<in> R\<inverse>; (y,b) \<in> R\<^sup>*; (y,c) \<in> R\<^sup>*\<rbrakk>
- \<Longrightarrow> \<exists>d. (b,d) \<in> R\<^sup>* \<and> (c,d) \<in> R\<^sup>*" by(rule less)
+ note IH = `\<And>y b c. \<lbrakk>(y,x) \<in> R\<inverse>; (y,b) \<in> R\<^sup>*; (y,c) \<in> R\<^sup>*\<rbrakk>
+ \<Longrightarrow> \<exists>d. (b,d) \<in> R\<^sup>* \<and> (c,d) \<in> R\<^sup>*`
have xc: "(x, c) \<in> R\<^sup>*" .
have xb: "(x, b) \<in> R\<^sup>*" .
thus ?case
@@ -223,11 +223,11 @@
assume y'c: "(y', c) \<in> R\<^sup>*"
assume xy': "(x, y') \<in> R"
with xy obtain u where u: "(y, u) \<in> R\<^sup>*" "(y', u) \<in> R\<^sup>*"
- by (blast dest:lc)
+ by (blast dest: lc)
from yb u y'c show ?thesis
- by(blast del: rtrancl_refl
- intro:rtrancl_trans
- dest:IH[OF xy[symmetric]] IH[OF xy'[symmetric]])
+ by (blast del: rtrancl_refl
+ intro: rtrancl_trans
+ dest: IH [OF xy [symmetric]] IH [OF xy' [symmetric]])
qed
qed
qed