Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Metis doesn't find an old proof in acceptable time now that higher-order equality reasoning is supported -- tuned proof script to help it
authorblanchet
Thu, 12 May 2011 15:29:19 +0200
changeset 42749 47f283fcf2ae
parent 42748 a37095d03074
child 42750 c8b1d9ee3758
Metis doesn't find an old proof in acceptable time now that higher-order equality reasoning is supported -- tuned proof script to help it
src/HOL/Auth/Kerberos_BAN.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Auth/Kerberos_BAN.thy	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy	Thu May 12 15:29:19 2011 +0200
@@ -288,7 +288,8 @@
 apply (unfold before_def)
 apply (erule rev_mp)
 apply (erule bankerberos.induct, simp_all add: takeWhile_tail)
-apply (metis length_rev set_rev takeWhile_void used_evs_rev)
+apply auto
+ apply (metis length_rev set_rev takeWhile_void used_evs_rev)+
 done
isabelle