[isabelle] About simplificaton



 hello,
         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  ?
                                                                       
                                                    Thanks 
                                                                       
                                                      Jean

Attachment: ns_bad.thy
Description: Binary data



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