# HG changeset patch
# User haftmann
# Date 1253541375 -7200
# Node ID 66ae4e8b1309ce19e9cc8c97902c69d301bd0b3f
# Parent  0264f360438d4d24b16ee637252caa9825bb2402
adapted proof

diff -r 0264f360438d -r 66ae4e8b1309 src/HOL/Auth/Guard/Extensions.thy
--- a/src/HOL/Auth/Guard/Extensions.thy	Mon Sep 21 15:35:24 2009 +0200
+++ b/src/HOL/Auth/Guard/Extensions.thy	Mon Sep 21 15:56:15 2009 +0200
@@ -11,7 +11,9 @@
 
 header {*Extensions to Standard Theories*}
 
-theory Extensions imports "../Event" begin
+theory Extensions
+imports "../Event"
+begin
 
 subsection{*Extensions to Theory @{text Set}*}
 
@@ -173,7 +175,7 @@
 subsubsection{*lemmas on analz*}
 
 lemma analz_UnI1 [intro]: "X:analz G ==> X:analz (G Un H)"
-by (subgoal_tac "G <= G Un H", auto dest: analz_mono)
+  by (subgoal_tac "G <= G Un H") (blast dest: analz_mono)+
 
 lemma analz_sub: "[| X:analz G; G <= H |] ==> X:analz H"
 by (auto dest: analz_mono)