| Fri, 14 Oct 2022 15:48:31 +0100 |
paulson |
Tidying of some very old proofs
|
file |
diff |
annotate
|
| Thu, 13 Oct 2022 15:38:32 +0100 |
paulson |
Elimination of the archaic ASCII syntax
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2016 09:33:54 +0200 |
nipkow |
"split add" -> "split"
|
file |
diff |
annotate
|
| Thu, 10 Dec 2015 21:39:33 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:54:56 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:32:36 +0200 |
blanchet |
updated news
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
|
file |
diff |
annotate
|
| Fri, 06 Sep 2013 10:56:40 +0200 |
noschinl |
use case_of_simps
|
file |
diff |
annotate
|
| Tue, 14 Feb 2012 21:19:39 +0100 |
wenzelm |
prefer high-level elim_format;
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:05:23 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Wed, 02 Feb 2011 14:11:26 +0000 |
paulson |
Introduction of metis calls and other cosmetic modifications.
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 18:38:30 +0200 |
bulwahn |
renewing specifications in HOL-Auth
|
file |
diff |
annotate
|
| Thu, 22 Jul 2010 18:08:39 +0200 |
wenzelm |
updated some headers;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Fri, 14 Aug 2009 17:26:11 +0100 |
paulson |
sledgehammer used to streamline protocol proofs
|
file |
diff |
annotate
|
| Mon, 16 Mar 2009 18:24:30 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| Mon, 16 Jun 2008 17:54:35 +0200 |
wenzelm |
eliminated OldGoals.inst;
|
file |
diff |
annotate
|
| Wed, 11 Jun 2008 18:02:25 +0200 |
wenzelm |
OldGoals.inst;
|
file |
diff |
annotate
|
| Wed, 01 Aug 2007 20:25:16 +0200 |
wenzelm |
tuned ML bindings (for multithreading);
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 15:44:51 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 23:42:35 +0200 |
wenzelm |
replaced syntax/translations by abbreviation;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2006 16:13:53 +0100 |
paulson |
a few more named lemmas
|
file |
diff |
annotate
|
| Wed, 26 Oct 2005 16:31:53 +0200 |
paulson |
tidied away duplicate thm
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Tue, 23 Sep 2003 15:41:33 +0200 |
paulson |
Removal of the Key_supply axiom (affects many possbility proofs) and minor
|
file |
diff |
annotate
|
| Thu, 24 Jul 2003 16:36:29 +0200 |
paulson |
Tidying and replacement of some axioms by specifications
|
file |
diff |
annotate
|
| Mon, 05 May 2003 18:22:01 +0200 |
paulson |
improved presentation of HOL/Auth theories
|
file |
diff |
annotate
|
| Tue, 29 Apr 2003 12:36:49 +0200 |
paulson |
tweaks
|
file |
diff |
annotate
|
| Sat, 26 Apr 2003 12:38:42 +0200 |
paulson |
converting more HOL-Auth to new-style theories
|
file |
diff |
annotate
|
| Fri, 25 Apr 2003 11:18:14 +0200 |
paulson |
Changes required by the certified email protocol
|
file |
diff |
annotate
|
| Mon, 06 Aug 2001 13:12:06 +0200 |
paulson |
three new theorems
|
file |
diff |
annotate
|
| Sat, 19 May 2001 12:19:23 +0200 |
paulson |
spelling check
|
file |
diff |
annotate
|
| Mon, 05 Mar 2001 12:31:31 +0100 |
paulson |
a few basic X-symbols
|
file |
diff |
annotate
|
| Fri, 02 Mar 2001 13:18:31 +0100 |
paulson |
conversion of Message.thy to Isar format
|
file |
diff |
annotate
|
| Tue, 13 Feb 2001 13:16:27 +0100 |
paulson |
partial conversion to Isar script style
|
file |
diff |
annotate
|
| Thu, 18 Mar 1999 10:41:00 +0100 |
paulson |
exchanged the order of Gets and Notes in datatype event
|
file |
diff |
annotate
|
| Tue, 09 Mar 1999 11:01:39 +0100 |
paulson |
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 13:03:20 +0200 |
berghofe |
Adapted to new datatype package.
|
file |
diff |
annotate
|
| Thu, 18 Sep 1997 13:24:04 +0200 |
paulson |
Global change: lost->bad and sees Spy->spies
|
file |
diff |
annotate
|
| Wed, 17 Sep 1997 16:37:27 +0200 |
paulson |
Spy can see Notes of the compromised agents
|
file |
diff |
annotate
|
| Mon, 14 Jul 1997 12:47:21 +0200 |
paulson |
Changing "lost" from a parameter of protocol definitions to a constant.
|
file |
diff |
annotate
|
| Fri, 11 Jul 1997 13:26:15 +0200 |
paulson |
Moving common declarations and proofs from theories "Shared"
|
file |
diff |
annotate
|
| Thu, 26 Sep 1996 12:50:48 +0200 |
paulson |
Introduction of "lost" argument
|
file |
diff |
annotate
|
| Tue, 03 Sep 1996 17:54:39 +0200 |
paulson |
Renaming and simplification
|
file |
diff |
annotate
|
| Wed, 21 Aug 1996 13:22:23 +0200 |
paulson |
Addition of message NS5
|
file |
diff |
annotate
|
| Tue, 20 Aug 1996 18:53:17 +0200 |
paulson |
Working version of NS, messages 1-4!
|
file |
diff |
annotate
|
| Tue, 20 Aug 1996 17:46:24 +0200 |
paulson |
Working version of NS, messages 1-3, WITH INTERLEAVING
|
file |
diff |
annotate
|
| Mon, 19 Aug 1996 11:19:55 +0200 |
paulson |
Renaming of functions, and tidying
|
file |
diff |
annotate
|
| Mon, 29 Jul 1996 18:31:39 +0200 |
paulson |
Works up to main theorem, then XXX...X
|
file |
diff |
annotate
|
| Fri, 26 Jul 1996 12:19:46 +0200 |
paulson |
Auth proofs work up to the XXX...
|
file |
diff |
annotate
|
| Thu, 11 Jul 1996 15:30:22 +0200 |
paulson |
Added Msg 3; works up to Says_Server_imp_Key_newK
|
file |
diff |
annotate
|
| Fri, 28 Jun 1996 15:26:39 +0200 |
paulson |
Proving safety properties of authentication protocols
|
file |
diff |
annotate
|