--- 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