| 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";