[isabelle] About simplificaton

         I'm  studying  the  proof  process of  NS_Public_Bad.thy in 
Isabelle.The content of file(  see  the attached file)is the
simplification rules used by auto  method  which is used to proving the
following lemma.I get the simplification rules  by 
"Isabele--setting--trace  simplifier".
                      lemma Spy_analz_priEK[simp]:
                       "evs \<in>ns_public\<Longrightarrow>(Key
(invkey(priEK A) \<in>analz(spies evs))=(A\<in>bad)"
                         by auto
           The simplification rules is verbose and very hard to
uderstand.Could anyone  interpret  the above simplification rules and
simplification process  ?

Attachment: ns_bad.thy
Description: Binary data

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.