| changeset 20217 | 25b068a99d2b |
| parent 19233 | 77ca20b0ed77 |
| child 20768 | 1d478c2d621f |
--- a/src/HOL/Auth/Guard/Extensions.thy Wed Jul 26 13:31:07 2006 +0200 +++ b/src/HOL/Auth/Guard/Extensions.thy Wed Jul 26 19:23:04 2006 +0200 @@ -231,7 +231,7 @@ "greatest_msg other = 0" lemma greatest_msg_is_greatest: "Nonce n:parts {X} ==> n <= greatest_msg X" -by (induct X, auto, arith+) +by (induct X, auto) subsubsection{*sets of keys*}