History log of /seL4-l4v-master/isabelle/src/HOL/Auth/KerberosV.thy
Revision Date Author Comments
# ed7a971e 05-Jan-2019 wenzelm <none@none>

isabelle update -u control_cartouches;


# f5796e6d 14-Feb-2018 wenzelm <none@none>

more symbols;


# 5385dbfa 16-Jan-2018 wenzelm <none@none>

standardized towards new-style formal comments: isabelle update_comments;


# feca4ab8 10-Dec-2015 wenzelm <none@none>

isabelle update_cartouches -c -t;


# 794edf80 02-Nov-2014 wenzelm <none@none>

modernized header uniformly as section;


# aff8c6a4 12-Feb-2014 blanchet <none@none>

adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
* * *
more transition of 'xxx_rec' to 'rec_xxx' and same for case
* * *
compile
* * *
'rename_tac's to avoid referring to generated names
* * *
more robust scripts with 'rename_tac'
* * *
'where' -> 'of'
* * *
'where' -> 'of'
* * *
renamed 'xxx_rec' to 'rec_xxx'


# 24890ce7 20-Mar-2012 blanchet <none@none>

optimized "metis" call


# f91b4242 28-Jun-2011 paulson <none@none>

tidied messy proofs


# 12379cec 18-Feb-2011 wenzelm <none@none>

modernized specifications;


# deac04eb 22-Jul-2010 wenzelm <none@none>

updated some headers;


# a5f328ca 12-May-2010 wenzelm <none@none>

modernized specifications;


# baea5702 01-Mar-2010 haftmann <none@none>

replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)


# 079cde2d 17-Oct-2009 wenzelm <none@none>

eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;


# 2d43315f 14-Aug-2009 paulson <none@none>

sledgehammer used to streamline protocol proofs


# 7715eb70 03-Dec-2008 wenzelm <none@none>

sources are not executable;


# 38095612 17-Mar-2008 wenzelm <none@none>

removed duplicate lemmas;


# 7b63d2a6 11-Jul-2007 berghofe <none@none>

Adapted to new inductive definition package.


# cd65d9bc 16-Nov-2006 wenzelm <none@none>

more robust syntax for definition/abbreviation/notation;


# 8d37dcbe 28-Sep-2006 wenzelm <none@none>

replaced syntax/translations by abbreviation;


# 26bd3ee2 01-Feb-2006 paulson <none@none>

new and updated protocol proofs by Giamp Bella