Replaced occurrence of fast_tac by Fast_tac .
authorberghofe
Fri, 21 Jun 1996 13:51:09 +0200
changeset 1823 e1458e1a9f80
parent 1822 c192d7dc22e7
child 1824 44254696843a
Replaced occurrence of fast_tac by Fast_tac .
src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Fri Jun 21 13:39:08 1996 +0200
+++ b/src/HOL/Nat.ML	Fri Jun 21 13:51:09 1996 +0200
@@ -462,7 +462,7 @@
         "!!m. Suc m <= n ==> m < n";
 by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
 by (cut_facts_tac [less_linear] 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "Suc_le_lessD";
 
 goal Nat.thy "(Suc m <= n) = (m < n)";