src/HOL/Lambda/Commutation.thy
changeset 18513 791b53bf4073
parent 18241 afdba6b3e383
child 19086 1b3780be6cc2
     1.1 --- a/src/HOL/Lambda/Commutation.thy	Fri Dec 23 18:36:27 2005 +0100
     1.2 +++ b/src/HOL/Lambda/Commutation.thy	Fri Dec 23 20:02:30 2005 +0100
     1.3 @@ -196,7 +196,7 @@
     1.4    and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow>
     1.5      \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
     1.6    shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
     1.7 -               \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
     1.8 +    \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
     1.9    using wf
    1.10  proof induct
    1.11    case (less x b c)