--- 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