| changeset 35422 | e74b6f3b950c |
| parent 35416 | d8d7d1b785af |
| child 41413 | 64cd30d6b0b8 |
--- a/src/HOL/ZF/LProd.thy Mon Mar 01 17:45:02 2010 +0100 +++ b/src/HOL/ZF/LProd.thy Mon Mar 01 17:45:19 2010 +0100 @@ -181,4 +181,4 @@ lemma "trans R \<Longrightarrow> (ah@a#at, bh@b#bt) \<in> lprod R \<Longrightarrow> (b, a) \<in> R \<or> a = b \<Longrightarrow> (ah@at, bh@bt) \<in> lprod R" oops -end \ No newline at end of file +end