removed junk;
authorwenzelm
Thu Mar 03 11:54:51 2016 +0100 (2016-03-03)
changeset 625028857237c3a90
parent 62501 98fa1f9a292f
child 62503 19afb533028e
removed junk;
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Nat.thy	Thu Mar 03 11:12:02 2016 +0100
     1.2 +++ b/src/HOL/Nat.thy	Thu Mar 03 11:54:51 2016 +0100
     1.3 @@ -1876,7 +1876,6 @@
     1.4    moreover from \<open>n < j\<close> have "Suc n \<le> j"
     1.5      by (simp add: Suc_le_eq)
     1.6    ultimately have "P (Suc n)"
     1.7 -  thm Suc.hyps TrueI Suc.prems
     1.8    proof (rule Suc.hyps)
     1.9      fix q
    1.10      assume "Suc n \<le> q"