src/HOL/IOA/IOA.ML
changeset 7499 23e090051cb8
parent 5184 9b8547a9496a
child 8114 09a7a180cc99
--- a/src/HOL/IOA/IOA.ML	Mon Sep 06 22:12:08 1999 +0200
+++ b/src/HOL/IOA/IOA.ML	Tue Sep 07 10:40:58 1999 +0200
@@ -70,7 +70,7 @@
    by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
   by (etac disjE 1);
    by (Asm_simp_tac 1);
-  by (forward_tac [less_not_sym] 1);
+  by (ftac less_not_sym 1);
   by (asm_simp_tac (simpset() addsimps [less_not_refl2,less_Suc_eq]) 1);
 qed "reachable_n";