History log of /seL4-l4v-master/l4v/isabelle/src/HOL/Auth/Kerberos_BAN_Gets.thy
Revision Date Author Comments
# f5796e6d 14-Feb-2018 wenzelm <none@none>

more symbols;


# 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'


# ad9e459c 11-Sep-2011 nipkow <none@none>

new fastforce replacing fastsimp - less confusing name


# f020e9da 09-Sep-2010 paulson <none@none>

Tidied up proofs using sledgehammer, also deleting unnecessary semicolons


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

updated some headers;


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

modernized specifications;


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

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


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

sources are not executable;


# 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