src/HOL/Auth/Kerberos_BAN_Gets.thy
2015-12-10 wenzelm 2015-12-10 isabelle update_cartouches -c -t;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-02-12 blanchet 2014-02-12 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'
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2010-09-09 paulson 2010-09-09 Tidied up proofs using sledgehammer, also deleting unnecessary semicolons
2010-07-22 wenzelm 2010-07-22 updated some headers;
2010-05-12 wenzelm 2010-05-12 modernized specifications;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-09-28 wenzelm 2006-09-28 replaced syntax/translations by abbreviation;
2006-02-01 paulson 2006-02-01 new and updated protocol proofs by Giamp Bella