# HG changeset patch
# User paulson
# Date 1182875320 -7200
# Node ID 332a9f5c7c29d9a801f3295c056bd62103b6fd93
# Parent  a1804e1370189436d378b8d6ae89e8bf65390424
simplified

diff -r a1804e137018 -r 332a9f5c7c29 src/HOL/Induct/Mutil.thy
--- 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