hyps better than prems
authorhaftmann
Wed Jun 21 10:26:39 2006 +0200 (2006-06-21)
changeset 1993316a5037f2d25
parent 19932 63bd0eeb4e0d
child 19934 8190655ea2d4
hyps better than prems
src/HOL/ex/Classpackage.thy
     1.1 --- a/src/HOL/ex/Classpackage.thy	Tue Jun 20 16:46:30 2006 +0200
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Wed Jun 21 10:26:39 2006 +0200
     1.3 @@ -166,7 +166,7 @@
     1.4  proof (induct n)
     1.5    case 0 with neutl npow_def show ?case by simp
     1.6  next
     1.7 -  case (Suc n) with prems assoc npow_def show ?case by simp
     1.8 +  case (Suc n) with Suc.hyps assoc npow_def show ?case by simp
     1.9  qed
    1.10  
    1.11  lemma (in monoid) nat_pow_pow: