--- a/src/HOL/Induct/Mutil.thy Tue Jun 26 15:48:24 2007 +0200
+++ b/src/HOL/Induct/Mutil.thy Tue Jun 26 18:28:40 2007 +0200
@@ -56,11 +56,11 @@
lemma Sigma_Suc1 [simp]:
"lessThan (Suc n) \<times> B = ({n} \<times> B) \<union> ((lessThan n) \<times> B)"
- by (auto simp add: lessThan_def)
+ by auto
lemma Sigma_Suc2 [simp]:
"A \<times> lessThan (Suc n) = (A \<times> {n}) \<union> (A \<times> (lessThan n))"
- by (auto simp add: lessThan_def)
+ by auto
lemma sing_Times_lemma: "({i} \<times> {n}) \<union> ({i} \<times> {m}) = {(i, m), (i, n)}"
by auto