# HG changeset patch
# User wenzelm
# Date 1256824433 -3600
# Node ID 2c77579e05238103d99f15d97c8f87728f7c3ba6
# Parent  1e1210f31207aa05045817e3bfce8725b31dbb59
tuned proof;

diff -r 1e1210f31207 -r 2c77579e0523 src/HOL/Auth/KerberosIV.thy
--- a/src/HOL/Auth/KerberosIV.thy	Thu Oct 29 13:21:38 2009 +0100
+++ b/src/HOL/Auth/KerberosIV.thy	Thu Oct 29 14:53:53 2009 +0100
@@ -780,7 +780,7 @@
 lemma u_NotexpiredSK_NotexpiredAK:
      "\<lbrakk> \<not> expiredSK Ts evs; servKlife + Ts <= authKlife + Ta \<rbrakk>
       \<Longrightarrow> \<not> expiredAK Ta evs"
-  by (metis nat_add_commute le_less_trans)
+  by (metis le_less_trans)
 
 
 subsection{* Reliability: friendly agents send something if something else happened*}