src/HOL/Auth/Event.ML
changeset 4477 b3e5857d8d99
parent 4266 dab1833cb26d
child 4686 74a12e86b20b
     1.1 --- a/src/HOL/Auth/Event.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOL/Auth/Event.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -27,7 +27,7 @@
     1.4  \      ((ALL A B X. ev = Says A B X --> P(sf A B X)) & \
     1.5  \       (ALL A X. ev = Notes A X --> P(nf A X)))";
     1.6  by (induct_tac "ev" 1);
     1.7 -by (Auto_tac());
     1.8 +by Auto_tac;
     1.9  qed "expand_event_case";
    1.10  
    1.11  goal thy "spies (Says A B X # evs) = insert X (spies evs)";