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 62502 8857237c3a90
parent 62481 b5d8e57826df
child 62608 19f87fa0cfcb 
--- a/src/HOL/Nat.thy	Thu Mar 03 11:12:02 2016 +0100
+++ b/src/HOL/Nat.thy	Thu Mar 03 11:54:51 2016 +0100
@@ -1876,7 +1876,6 @@
   moreover from \<open>n < j\<close> have "Suc n \<le> j"
     by (simp add: Suc_le_eq)
   ultimately have "P (Suc n)"
-  thm Suc.hyps TrueI Suc.prems
   proof (rule Suc.hyps)
     fix q
     assume "Suc n \<le> q"
isabelle