changeset 20217 | 25b068a99d2b |
parent 16417 | 9bc16273c2d4 |
child 35416 | d8d7d1b785af |
--- a/src/HOL/Auth/Guard/Guard_Public.thy Wed Jul 26 13:31:07 2006 +0200 +++ b/src/HOL/Auth/Guard/Guard_Public.thy Wed Jul 26 19:23:04 2006 +0200 @@ -95,7 +95,7 @@ apply (induct evs, auto simp: initState.simps) apply (drule used_sub_parts_used, safe) apply (drule greatest_msg_is_greatest, arith) -by (simp, arith) +by simp subsubsection{*function giving a new nonce*} @@ -171,4 +171,4 @@ apply (frule_tac A=A in priK_analz_iff_bad) by (simp add: knows_decomp)+ -end \ No newline at end of file +end