Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/EfficientNat.thy
changeset 23394 474ff28210c0
parent 23365 f31794033ae1
child 23438 dd824e86fa8a 
--- a/src/HOL/Library/EfficientNat.thy	Thu Jun 14 23:04:36 2007 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Thu Jun 14 23:04:39 2007 +0200
@@ -48,13 +48,13 @@
   fixes k
   assumes "k \<ge> 0"
   shows "number_of k = nat_of_int (number_of k)"
-  unfolding nat_of_int_def [OF prems] nat_number_of_def number_of_is_id ..
+  unfolding nat_of_int_def [OF assms] nat_number_of_def number_of_is_id ..
 
 lemma nat_of_int_of_number_of_aux:
   fixes k
   assumes "Numeral.Pls \<le> k \<equiv> True"
   shows "k \<ge> 0"
-  using prems unfolding Pls_def by simp
+  using assms unfolding Pls_def by simp
 
 lemma nat_of_int_int:
   "nat_of_int (int' n) = n"
isabelle