# HG changeset patch
# User wenzelm
# Date 1457002491 -3600
# Node ID 8857237c3a90cabcfa32c033dc5753ac4138ad13
# Parent  98fa1f9a292fe621dc6485e702327162a8be0581
removed junk;

diff -r 98fa1f9a292f -r 8857237c3a90 src/HOL/Nat.thy
--- 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"