Removed Fast_tac made redundant by addition of de Morgan laws
authorpaulson
Thu Oct 10 10:45:20 1996 +0200 (1996-10-10)
changeset 2081c2da3ca231ab
parent 2080 12eed4cec935
child 2082 8659e3063a30
Removed Fast_tac made redundant by addition of de Morgan laws
src/HOL/Nat.ML
     1.1 --- a/src/HOL/Nat.ML	Wed Oct 09 13:50:28 1996 +0200
     1.2 +++ b/src/HOL/Nat.ML	Thu Oct 10 10:45:20 1996 +0200
     1.3 @@ -450,7 +450,6 @@
     1.4  
     1.5  goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
     1.6  by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
     1.7 -by (Fast_tac 1);
     1.8  qed "Suc_leD";
     1.9  
    1.10  (* stronger version of Suc_leD *)