src/HOL/Auth/Yahalom.thy
Sat, 05 Jan 2019 17:24:33 +0100 wenzelm isabelle update -u control_cartouches;
Thu, 15 Feb 2018 12:11:00 +0100 wenzelm more symbols;
Tue, 16 Jan 2018 09:30:00 +0100 wenzelm standardized towards new-style formal comments: isabelle update_comments;
Tue, 19 Dec 2017 13:58:12 +0100 wenzelm isabelle update_cartouches -c -t;
Mon, 24 Oct 2016 14:31:05 +0100 paulson "subgoal" examples
Mon, 28 Dec 2015 23:13:33 +0100 wenzelm more symbols;
Thu, 10 Dec 2015 21:39:33 +0100 wenzelm isabelle update_cartouches -c -t;
Wed, 25 Mar 2015 10:44:57 +0100 wenzelm prefer local fixes;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Sun, 20 Nov 2011 21:05:23 +0100 wenzelm eliminated obsolete "standard";
Fri, 27 Aug 2010 10:56:46 +0200 haftmann formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
Thu, 22 Jul 2010 18:08:39 +0200 wenzelm updated some headers;
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Fri, 14 Aug 2009 21:36:14 +0200 krauss removed atp_minimize invocation
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) -30 tip