1.1 --- a/src/HOL/SET_Protocol/Purchase.thy	Sun May 15 17:06:35 2011 +0200
     1.2 +++ b/src/HOL/SET_Protocol/Purchase.thy	Sun May 15 17:45:53 2011 +0200
     1.3 @@ -484,7 +484,7 @@
     1.4      K (SIMPLE_METHOD'' quant (fn i =>
     1.5        EVERY [ftac @{thm Gets_certificate_valid} i,
     1.6               assume_tac i, REPEAT (hyp_subst_tac i)])))
     1.7 -*} ""
     1.8 +*}
     1.9  
    1.10  
    1.11  subsection{*Proofs on Symmetric Keys*}