--- a/src/HOL/Auth/Guard/P1.thy Fri Feb 18 15:46:13 2011 +0100
+++ b/src/HOL/Auth/Guard/P1.thy Fri Feb 18 16:07:32 2011 +0100
@@ -1,17 +1,11 @@
-(******************************************************************************
-from G. Karjoth, N. Asokan and C. Gulcu
-"Protecting the computation results of free-roaming agents"
-Mobiles Agents 1998, LNCS 1477
+(* Title: HOL/Auth/Guard/P1.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
-date: february 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+From G. Karjoth, N. Asokan and C. Gulcu
+"Protecting the computation results of free-roaming agents"
+Mobiles Agents 1998, LNCS 1477.
+*)
header{*Protocol P1*}