isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

Now there are TWO spaces after each full stop, so that the Emacs sentence
1997-07-02, by paulson
Now there are TWO spaces after each full stop, so that the Emacs sentence
1997-07-02, by paulson
Added the following lemmas tp Divides and a few others to Arith and NatDef:
1997-07-02, by nipkow
Tidying; also simplified the lemma Says_Server_not
1997-07-01, by paulson
New theory TLS
1997-07-01, by paulson
Deleted a redundant A~=B in rules that refer to a previous event
1997-07-01, by paulson
More realistic model: the Spy can compute clientK and serverK
1997-07-01, by paulson
Reordered rules in analz_image_freshK_ss to improve clarity
1997-07-01, by paulson
Removal of the obsolete newN function
1997-07-01, by paulson
New theorem priK_inj_eq, injectivity of priK
1997-07-01, by paulson
spy_analz_tac: Restored iffI to the list of rules used to break down
1997-07-01, by paulson
New theory TLS
1997-07-01, by paulson
Baby TLS. Proofs work, but model seems unrealistic
1997-07-01, by paulson
New and stronger lemmas; more default simp/cla rules
1997-07-01, by paulson
Deleted the obsolete operators newK, newN and nPair
1997-07-01, by paulson
Now the possibility proof calls the appropriate tactic
1997-07-01, by paulson
Added a comment
1997-07-01, by paulson
Now Collect_mem_eq is a default simprule (how could it have ever been omitted?
1997-07-01, by paulson
New laws for the "lists" operator
1997-07-01, by paulson
More concat lemmas.
1997-06-30, by nipkow
Corrected indentations and margins after the renaming of "set_of_list"
1997-06-27, by paulson
set_of_list -> set
1997-06-26, by nipkow
Trivial changes in connection with the Yahalom paper.
1997-06-26, by paulson
oops;
1997-06-26, by wenzelm
rearrange pages of ps file to be printed as booklet (duplex);
1997-06-26, by wenzelm
amdI -> admI2
1997-06-26, by nipkow
Tuned Franz's proofs.
1997-06-26, by nipkow
Removal of structure Context and its replacement by a theorem list of
1997-06-23, by paulson
Removal of COND_CONG, which is just if_cong RS eq_reflection
1997-06-23, by paulson
Ran expandshort
1997-06-23, by paulson
New "congs" keyword for recdef theory section
1997-06-23, by paulson
removed old Makefile;
1997-06-20, by wenzelm
removed;
1997-06-20, by wenzelm
removed old Makefile;
1997-06-20, by wenzelm
removed old Makefile and compat files;
1997-06-20, by wenzelm
Made proofs more concise by replacing calls to spy_analz_tac by uses of
1997-06-19, by paulson
Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
1997-06-19, by paulson
New comments; a tidied proof
1997-06-19, by paulson
Two new rewrite rules--NOT included by default\!
1997-06-19, by paulson
Defines KeyWithNonce, which is used to prove the secrecy of NB
1997-06-18, by paulson
Addition of not_imp (which pushes negation into implication) as a default
1997-06-18, by paulson
Corrected Title in header lines
1997-06-18, by paulson
Streamlined proofs of the secrecy of NB and added authentication of A and B
1997-06-18, by paulson
Removed Says_Crypt_lost and Says_Crypt_not_lost.
1997-06-18, by paulson
Removed Says_Crypt_lost and Says_Crypt_not_lost.
1997-06-18, by paulson
Adapted proofs to the removal of Says_Crypt_lost and Says_Crypt_not_lost
1997-06-18, by paulson
Deleted spurious reference to Spy_not_see_NB, which by chance was defined
1997-06-18, by paulson
converse -> ^-1
1997-06-17, by nipkow
Type constraint added to ensure that "length" refers to lists. Maybe should
1997-06-16, by paulson
Replacing the primrec definition of "length" by a translation to the built-in
1997-06-16, by paulson
Tuned wf_iff_no_infinite_down_chain proof, based on Konrads ideas.
1997-06-13, by nipkow
changed compatible definition;
1997-06-13, by mueller
added deadlock
1997-06-12, by mueller
added deadlock freedom, polished definitions and proofs
1997-06-12, by mueller
Strengthened and streamlined the Yahalom proofs
1997-06-09, by paulson
Useful new lemma
1997-06-09, by paulson
eliminated non-ASCII;
1997-06-06, by wenzelm
Added
1997-06-06, by nipkow
improved function 'nonreserved'
1997-06-06, by oheimb
Removed a few redundant additions of simprules or classical rules
1997-06-06, by paulson

less more | (0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle