| changeset 5758 | 27a2b36efd95 |
| parent 5648 | fe887910e32e |
| child 6570 | a7d7985050a9 |
--- a/src/HOL/UNITY/NSP_Bad.ML Fri Oct 23 20:36:21 1998 +0200 +++ b/src/HOL/UNITY/NSP_Bad.ML Fri Oct 23 20:44:34 1998 +0200 @@ -77,7 +77,7 @@ Goal "s : reachable Nprg ==> (Key (priK A) : parts (spies s)) = (A : bad)"; by (etac reachable.induct 1); -by Auto_tac; +by (ALLGOALS Force_tac); qed "Spy_see_priK"; Addsimps [Spy_see_priK];