src/HOL/Auth/Yahalom.thy
Thu, 13 Aug 2009 17:19:42 +0100 paulson Removal of redundant settings of unification trace and search bounds.
Wed, 11 Jul 2007 11:14:51 +0200 berghofe Adapted to new inductive definition package.
Wed, 04 Jan 2006 16:13:53 +0100 paulson a few more named lemmas
Fri, 07 Oct 2005 20:41:10 +0200 nipkow changes due to new neq_simproc in simpdata.ML
Thu, 15 Sep 2005 17:16:55 +0200 wenzelm fixed document;
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Fri, 26 Sep 2003 10:34:28 +0200 paulson Conversion of all main protocols from "Shared" to "Public".
Tue, 23 Sep 2003 15:41:33 +0200 paulson Removal of the Key_supply axiom (affects many possbility proofs) and minor
Mon, 05 May 2003 18:22:01 +0200 paulson improved presentation of HOL/Auth theories
Sat, 26 Apr 2003 12:38:42 +0200 paulson converting more HOL-Auth to new-style theories
Sat, 17 Aug 2002 14:55:08 +0200 paulson tidying of Isar scripts
Wed, 03 Oct 2001 20:54:16 +0200 wenzelm tuned parentheses in relational expressions;
Thu, 12 Apr 2001 12:45:05 +0200 paulson converted many HOL/Auth theories to Isar scripts
Tue, 27 Feb 2001 16:13:23 +0100 paulson Some X-symbols for <notin>, <noteq>, <forall>, <exists>
Wed, 10 Mar 1999 10:42:57 +0100 paulson updating both Yahalom protocols to the Gets model
less more (0) -15 tip