--- a/src/HOL/Auth/Event.ML Fri Nov 21 12:14:47 1997 +0100
+++ b/src/HOL/Auth/Event.ML Fri Nov 21 12:15:10 1997 +0100
@@ -129,10 +129,10 @@
this information isn't needed, the proof will be much shorter, since
it will omit complicated reasoning about analz.*)
val analz_mono_contra_tac =
- let val impI' = read_instantiate_sg (sign_of thy)
- [("P", "?Y ~: analz (sees ?A ?evs)")] impI;
+ let val analz_impI = read_instantiate_sg (sign_of thy)
+ [("P", "?Y ~: analz (spies ?evs)")] impI;
in
- rtac impI THEN'
+ rtac analz_impI THEN'
REPEAT1 o
(dresolve_tac
[spies_subset_spies_Says RS analz_mono RS contra_subsetD,