changeset 4473 | 803d1e302af1 |
parent 4423 | a129b817b58a |
child 4477 | b3e5857d8d99 |
--- a/src/HOLCF/IOA/meta_theory/Automata.ML Tue Dec 23 11:47:13 1997 +0100 +++ b/src/HOLCF/IOA/meta_theory/Automata.ML Tue Dec 23 11:49:46 1997 +0100 @@ -205,7 +205,7 @@ by (eres_inst_tac [("x","a")] allE 1); by (eres_inst_tac [("x","a")] allE 1); by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1); -by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1); +by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1); by (dtac inpAAactB_is_inpBoroutB 1); back(); by (assume_tac 1);