# HG changeset patch
# User paulson
# Date 844937120 -7200
# Node ID c2da3ca231aba705e2efa6c6a5a37bdbd2eb9524
# Parent  12eed4cec93576215f12b0710a58d8e51e8ad126
Removed Fast_tac made redundant by addition of de Morgan laws

diff -r 12eed4cec935 -r c2da3ca231ab src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Wed Oct 09 13:50:28 1996 +0200
+++ b/src/HOL/Nat.ML	Thu Oct 10 10:45:20 1996 +0200
@@ -450,7 +450,6 @@
 
 goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
 by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
-by (Fast_tac 1);
 qed "Suc_leD";
 
 (* stronger version of Suc_leD *)