src/HOL/Auth/Guard/List_Msg.thy

 subsection{*Implementation of Lists by Messages*}
 
 subsubsection{*nil is represented by any message which is not a pair*}
 
 abbreviation (input)
-  cons :: "msg => msg => msg"
+  cons :: "msg => msg => msg" where
   "cons x l == {|x,l|}"
 
 subsubsection{*induction principle*}
 
 lemma lmsg_induct: "[| !!x. not_MPair x ==> P x; !!x l. P l ==> P (cons x l) |]

 subsection{*Agent Lists*}
 
 subsubsection{*set of well-formed agent-list messages*}
 
 abbreviation
-  nil :: msg
+  nil :: msg where
   "nil == Number 0"
 
 consts agl :: "msg set"
 
 inductive agl