# HG changeset patch
# User wenzelm
# Date 1027097077 -7200
# Node ID ea1b3afb147e379478bd11fbf4a4ff17c67e9379
# Parent  dbb608cd11c4ea0bdf4a694e60c5eada5329d9c7
*** empty log message ***

diff -r dbb608cd11c4 -r ea1b3afb147e src/HOL/NumberTheory/IntFact.thy
--- a/src/HOL/NumberTheory/IntFact.thy	Fri Jul 19 18:44:36 2002 +0200
+++ b/src/HOL/NumberTheory/IntFact.thy	Fri Jul 19 18:44:37 2002 +0200
@@ -39,10 +39,7 @@
 
 lemma setprod_insert [simp]:
     "finite A ==> a \<notin> A ==> setprod (insert a A) = a * setprod A"
-  apply (unfold setprod_def)
-  apply (simp add: zmult_left_commute LC.fold_insert [OF LC_axioms.intro])
-  done
-
+  by (simp add: setprod_def zmult_left_commute LC.fold_insert [OF LC.intro, OF LC_axioms.intro])
 
 text {*
   \medskip @{term d22set} --- recursively defined set including all