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.
removed junk;
authorwenzelm
Thu, 03 Mar 2016 11:54:51 +0100
changeset 62502 8857237c3a90
parent 62501 98fa1f9a292f
child 62503 19afb533028e
removed junk;
src/HOL/Nat.thy file | annotate | diff | comparison | revisions 
--- 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