src/HOL/Auth/Smartcard/Smartcard.thy
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-09-08 haftmann 2010-09-08 modernized primrec
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-21 haftmann 2009-09-21 common base for protocols with symmetric keys
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-03-16 wenzelm 2009-03-16 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2007-08-01 wenzelm 2007-08-01 tuned ML bindings (for multithreading);
2007-07-21 wenzelm 2007-07-21 tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
2007-02-07 berghofe 2007-02-07 Adapted to changes in Finite_Set theory.
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2006-07-08 wenzelm 2006-07-08 tactic/method simpset: maintain proper context;
2006-02-01 paulson 2006-02-01 new and updated protocol proofs by Giamp Bella