#
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
#
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
#
feca4ab8 |
|
10-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
aff8c6a4 |
|
12-Feb-2014 |
blanchet <none@none> |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
|
#
12379cec |
|
18-Feb-2011 |
wenzelm <none@none> |
modernized specifications;
|
#
deac04eb |
|
22-Jul-2010 |
wenzelm <none@none> |
updated some headers;
|
#
a4e4c091 |
|
13-Jul-2010 |
paulson <none@none> |
corrected mixfix declarations and tidied proofs
|
#
a5f328ca |
|
12-May-2010 |
wenzelm <none@none> |
modernized specifications;
|
#
baea5702 |
|
01-Mar-2010 |
haftmann <none@none> |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
#
dabf5b98 |
|
29-Oct-2009 |
wenzelm <none@none> |
tuned proof;
|
#
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
|
#
bdfef9f3 |
|
28-Aug-2009 |
wenzelm <none@none> |
removed spurious invocations of atp_minimize;
|
#
da0a2209 |
|
13-Aug-2009 |
paulson <none@none> |
Demonstrations of sledgehammer in protocol proofs.
|
#
7b63d2a6 |
|
11-Jul-2007 |
berghofe <none@none> |
Adapted to new inductive definition package.
|
#
cd65d9bc |
|
16-Nov-2006 |
wenzelm <none@none> |
more robust syntax for definition/abbreviation/notation;
|
#
8d37dcbe |
|
28-Sep-2006 |
wenzelm <none@none> |
replaced syntax/translations by abbreviation;
|
#
26bd3ee2 |
|
01-Feb-2006 |
paulson <none@none> |
new and updated protocol proofs by Giamp Bella
|
#
b66236eb |
|
13-Jul-2005 |
paulson <none@none> |
generlization of some "nat" theorems
|
#
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
#
49de6382 |
|
15-Jun-2004 |
paulson <none@none> |
slight speed improvement
|
#
5442a36e |
|
26-Sep-2003 |
paulson <none@none> |
Conversion of all main protocols from "Shared" to "Public". Removal of Key_supply_ax: modifications to possibility theorems. Improved presentation.
|
#
d66531ec |
|
23-Sep-2003 |
paulson <none@none> |
Removal of the Key_supply axiom (affects many possbility proofs) and minor changes
|
#
9bfbac32 |
|
04-Sep-2003 |
paulson <none@none> |
conversion of HOL/Auth/KerberosIV to new-style theory
|
#
05b61f85 |
|
17-Aug-2002 |
paulson <none@none> |
tidying of Isar scripts
|
#
f96783a0 |
|
05-Oct-2001 |
wenzelm <none@none> |
* sane numerals (stage 2): plain "num" syntax (removed "#");
|
#
6ddaa347 |
|
05-Oct-2001 |
wenzelm <none@none> |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
|
#
f42afa45 |
|
06-Aug-2001 |
paulson <none@none> |
Changed 1 to 1' (= Suc 0)
|
#
22bc9d8c |
|
27-Feb-2001 |
paulson <none@none> |
Some X-symbols for <notin>, <noteq>, <forall>, <exists> Streamlining of Yahalom proofs Removal of redundant proofs
|
#
ca738d3d |
|
20-Apr-1999 |
paulson <none@none> |
addition of Kerberos IV example
|