src/HOL/Auth/Smartcard/ShoupRubin.thy
Fri, 18 Feb 2011 15:46:13 +0100 wenzelm modernized specifications;
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Thu, 23 Jul 2009 18:44:09 +0200 wenzelm renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
Mon, 16 Mar 2009 18:24:30 +0100 wenzelm simplified method setup;
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Wed, 01 Aug 2007 20:25:16 +0200 wenzelm tuned ML bindings (for multithreading);
Sat, 21 Jul 2007 23:25:00 +0200 wenzelm tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
Wed, 11 Jul 2007 11:14:51 +0200 berghofe Adapted to new inductive definition package.
Wed, 29 Nov 2006 15:44:51 +0100 wenzelm simplified method setup;
Sat, 08 Jul 2006 12:54:36 +0200 wenzelm tactic/method simpset: maintain proper context;
Wed, 01 Feb 2006 15:22:02 +0100 paulson new and updated protocol proofs by Giamp Bella
less more (0) tip