# HG changeset patch # User haftmann # Date 1150878399 -7200 # Node ID 16a5037f2d25cdb5fecdc0826feda98be078f8bc # Parent 63bd0eeb4e0d0179f5ae3388b7a4360b445e205b hyps better than prems diff -r 63bd0eeb4e0d -r 16a5037f2d25 src/HOL/ex/Classpackage.thy --- a/src/HOL/ex/Classpackage.thy Tue Jun 20 16:46:30 2006 +0200 +++ b/src/HOL/ex/Classpackage.thy Wed Jun 21 10:26:39 2006 +0200 @@ -166,7 +166,7 @@ proof (induct n) case 0 with neutl npow_def show ?case by simp next - case (Suc n) with prems assoc npow_def show ?case by simp + case (Suc n) with Suc.hyps assoc npow_def show ?case by simp qed lemma (in monoid) nat_pow_pow: