| #
ab32308e |
|
21-Jan-2019 |
paulson <lp15@cam.ac.uk> |
renamings and new material
|
| #
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;
|
| #
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
6688eecc |
|
17-Feb-2016 |
haftmann <none@none> |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
| #
ce5e1da3 |
|
28-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
| #
feca4ab8 |
|
10-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
8083303a |
|
23-Mar-2015 |
wenzelm <none@none> |
support 'for' fixes in rule_tac etc.;
|
| #
2d6c364b |
|
20-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
4e1305ff |
|
19-Mar-2015 |
wenzelm <none@none> |
more position information;
|
| #
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
5fc26177 |
|
11-Sep-2014 |
blanchet <none@none> |
updated news
|
| #
d2ddb3a1 |
|
09-Sep-2014 |
blanchet <none@none> |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
| #
61b92429 |
|
26-Jun-2014 |
paulson <lp15@cam.ac.uk> |
tiny refinements
|
| #
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
| #
e4f1682f |
|
12-Apr-2013 |
wenzelm <none@none> |
removed historic comments;
|
| #
f4961062 |
|
20-Nov-2011 |
wenzelm <none@none> |
eliminated obsolete "standard";
|
| #
ccb67976 |
|
12-Aug-2011 |
huffman <none@none> |
make more HOL theories work with separate set type
|
| #
8d662244 |
|
27-Jun-2011 |
paulson <none@none> |
keyfree: The set of key-free messages (and associated theorems)
|
| #
2f53d74a |
|
13-May-2011 |
wenzelm <none@none> |
proper Proof.context for classical tactics;
reduced claset to snapshot of classical context;
discontinued clasimpset;
|
| #
188dbb7e |
|
26-Apr-2011 |
wenzelm <none@none> |
simplified/modernized method setup;
|
| #
12379cec |
|
18-Feb-2011 |
wenzelm <none@none> |
modernized specifications;
|
| #
898b7628 |
|
02-Feb-2011 |
paulson <none@none> |
Introduction of metis calls and other cosmetic modifications.
|
| #
4ca87fa3 |
|
08-Sep-2010 |
paulson <none@none> |
tidied using inductive_simps
|
| #
deac04eb |
|
22-Jul-2010 |
wenzelm <none@none> |
updated some headers;
|
| #
4dca2c8c |
|
04-Mar-2010 |
paulson <none@none> |
Simplified a couple of proofs and corrected a comment
|
| #
baea5702 |
|
01-Mar-2010 |
haftmann <none@none> |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
| #
94b29512 |
|
11-Feb-2010 |
wenzelm <none@none> |
modernized syntax/translations;
|
| #
3403212c |
|
08-Feb-2010 |
wenzelm <none@none> |
modernized some syntax translations;
|
| #
38dd4864 |
|
24-Dec-2009 |
paulson <none@none> |
tidied proofs
|
| #
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
| #
a4b600c4 |
|
23-Jul-2009 |
wenzelm <none@none> |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
| #
2b61dda1 |
|
21-Jul-2009 |
haftmann <none@none> |
Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy
|
| #
2251533a |
|
20-Mar-2009 |
wenzelm <none@none> |
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
|
| #
b1258973 |
|
16-Mar-2009 |
wenzelm <none@none> |
simplified method setup;
|
| #
77d6b267 |
|
13-Mar-2009 |
wenzelm <none@none> |
unified type Proof.method and pervasive METHOD combinators;
|
| #
3b2c1f6d |
|
27-Oct-2008 |
paulson <none@none> |
metis proof
|
| #
fe16ec1f |
|
16-Jun-2008 |
wenzelm <none@none> |
pervasive RuleInsts;
|
| #
a5551838 |
|
16-Jun-2008 |
wenzelm <none@none> |
eliminated OldGoals.inst;
|
| #
6284a6de |
|
11-Jun-2008 |
wenzelm <none@none> |
OldGoals.inst;
|
| #
9769db9f |
|
11-Jun-2008 |
wenzelm <none@none> |
RuleInsts.res_inst_tac with proper context;
|
| #
afeb804a |
|
10-Jun-2008 |
haftmann <none@none> |
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
|
| #
e4cc2125 |
|
07-May-2008 |
berghofe <none@none> |
Replaced blast by fast in proof of parts_singleton, since blast looped
because of the new encoding of sets.
|
| #
bd98015c |
|
19-Mar-2008 |
wenzelm <none@none> |
more antiquotations;
|
| #
df5ccfe2 |
|
01-Aug-2007 |
wenzelm <none@none> |
tuned ML bindings (for multithreading);
|
| #
7b63d2a6 |
|
11-Jul-2007 |
berghofe <none@none> |
Adapted to new inductive definition package.
|
| #
31b1ad8b |
|
06-May-2007 |
haftmann <none@none> |
dropped legacy ML binding
|
| #
e0f5e1ab |
|
09-Mar-2007 |
haftmann <none@none> |
*** empty log message ***
|
| #
f7800759 |
|
29-Nov-2006 |
wenzelm <none@none> |
simplified method setup;
|
| #
e322a44b |
|
20-Sep-2006 |
paulson <none@none> |
tidied
|
| #
9004ff29 |
|
22-Dec-2005 |
paulson <none@none> |
shorter proof
|
| #
b3380a60 |
|
30-Sep-2005 |
paulson <none@none> |
theorems need names
|
| #
d84f4588 |
|
28-Sep-2005 |
paulson <none@none> |
streamlined theory; conformance to recent publication
|
| #
6624e62e |
|
13-Jul-2005 |
paulson <none@none> |
tidied
|
| #
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
|
| #
0d9b3ba0 |
|
11-Jul-2004 |
wenzelm <none@none> |
local_cla/simpset_of;
|
| #
d66531ec |
|
23-Sep-2003 |
paulson <none@none> |
Removal of the Key_supply axiom (affects many possbility proofs) and minor
changes
|
| #
91c79bda |
|
04-Sep-2003 |
paulson <none@none> |
new, separate specifications
|
| #
05eb17d2 |
|
12-Aug-2003 |
paulson <none@none> |
ZhouGollmann: new example (fair non-repudiation protocol)
|
| #
f6663d03 |
|
24-Jul-2003 |
paulson <none@none> |
Tidying and replacement of some axioms by specifications
|
| #
7a4d9400 |
|
05-May-2003 |
paulson <none@none> |
improved presentation of HOL/Auth theories
|
| #
63be96be |
|
25-Apr-2003 |
paulson <none@none> |
converting more HOL-Auth to new-style theories
|
| #
c5f9f5e4 |
|
25-Apr-2003 |
paulson <none@none> |
Changes required by the certified email protocol
Public-key model now provides separate signature/encryption keys and also
long-term symmetric keys.
|
| #
a887046d |
|
27-Apr-2001 |
paulson <none@none> |
better treatment of methods: uses Method.ctxt_args to refer to current
simpset and claset. Needed to fix problems with Recur.thy
|
| #
153d8df2 |
|
23-Apr-2001 |
paulson <none@none> |
(rough) conversion of Auth/Recur to Isar format
|
| #
f88893dc |
|
11-Apr-2001 |
paulson <none@none> |
converted many HOL/Auth theories to Isar scripts
|
| #
d73180c4 |
|
09-Apr-2001 |
paulson <none@none> |
new theorem Fake_parts_insert_in_Un
|
| #
68aabf0f |
|
29-Mar-2001 |
paulson <none@none> |
misc tidying; changing the predicate isSymKey to the set symKeys
|
| #
0c13cd01 |
|
04-Mar-2001 |
paulson <none@none> |
a few basic X-symbols
|
| #
158d88c6 |
|
02-Mar-2001 |
paulson <none@none> |
conversion of Message.thy to Isar format
|
| #
609bc635 |
|
09-Jan-2001 |
nipkow <none@none> |
`` -> ` and ``` -> ``
|
| #
904a7109 |
|
23-Aug-2000 |
paulson <none@none> |
xsymbols for {| and |}
|
| #
02b5dd02 |
|
21-Jul-1999 |
paulson <none@none> |
tweaked proofs to handle new freeness reasoning for data c onstructors
|
| #
06114d59 |
|
10-Jun-1999 |
paulson <none@none> |
new translation to allow images over Nonce
|
| #
843745b5 |
|
15-Oct-1998 |
paulson <none@none> |
parent is Main
|
| #
cea77ac9 |
|
03-Aug-1998 |
paulson <none@none> |
Better comments
|
| #
df41c559 |
|
24-Jul-1998 |
berghofe <none@none> |
Adapted to new datatype package.
|
| #
a907175c |
|
30-Jun-1998 |
berghofe <none@none> |
Adapted to new inductive definition package.
|
| #
51a4c5de |
|
10-Sep-1997 |
paulson <none@none> |
Split base cases from "msg" to "atomic" in order
to reduce the number of freeness theorems
|
| #
5b1e40e3 |
|
16-Jan-1997 |
paulson <none@none> |
Now with Andy Gordon's treatment of freshness to replace newN/K
|
| #
5cd53b91 |
|
07-Jan-1997 |
paulson <none@none> |
Incorporation of HPair into Message
|
| #
e9d38542 |
|
13-Dec-1996 |
paulson <none@none> |
Addition of the Hash constructor
Strengthening spy_analz_tac
|
| #
ad1324da |
|
29-Nov-1996 |
paulson <none@none> |
Swapped arguments of Crypt (for clarity and because it is conventional)
|
| #
a3eca20f |
|
24-Oct-1996 |
paulson <none@none> |
Removal of unused predicate isSpy
|
| #
e2feb658 |
|
25-Sep-1996 |
paulson <none@none> |
Introduction of "lost" argument
Changed Enemy -> Spy
Ran expandshort
|
| #
d56e5977 |
|
23-Sep-1996 |
paulson <none@none> |
Simplification of definition of synth
|
| #
433d2a00 |
|
03-Sep-1996 |
paulson <none@none> |
Fixed pretty-printing of {|...|}
|
| #
49ed9cfd |
|
19-Aug-1996 |
paulson <none@none> |
Renaming of functions, and tidying
|
| #
782f2f44 |
|
28-Jun-1996 |
paulson <none@none> |
Proving safety properties of authentication protocols
|