Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
hyps better than prems
authorhaftmann
Wed, 21 Jun 2006 10:26:39 +0200
changeset 19933 16a5037f2d25
parent 19932 63bd0eeb4e0d
child 19934 8190655ea2d4
hyps better than prems
src/HOL/ex/Classpackage.thy file | annotate | diff | comparison | revisions 
--- 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:
isabelle