# HG changeset patch
# User wenzelm
# Date 1284125809 -7200
# Node ID cc7abfe6d5e7ea432441a29ed8bdf40a7cfcf87a
# Parent  f263522ab226aa02eff1cb575972c65ed4b98adc
removed spurious addition from 9e58f0499f57;

diff -r f263522ab226 -r cc7abfe6d5e7 src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Fri Sep 10 15:17:44 2010 +0200
+++ b/src/HOL/Auth/Public.thy	Fri Sep 10 15:36:49 2010 +0200
@@ -199,8 +199,6 @@
 knowledge of the Spy.  All other agents are automata, merely following the
 protocol.*}
 
-term initState_Server
-
 overloading
   initState \<equiv> initState
 begin