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/Nat.thy
changeset 14348 744c868ee0b7
parent 14341 a09441bd4f1e
child 14691 e1eedc8cad37 
--- a/src/HOL/Nat.thy	Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Nat.thy	Fri Jan 09 10:46:18 2004 +0100
@@ -771,6 +771,7 @@
 instance nat :: ordered_semiring
 proof
   fix i j k :: nat
+  show "0 < (1::nat)" by simp
   show "i \<le> j ==> k + i \<le> k + j" by simp
   show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
 qed
isabelle