Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-1000
-120
+120
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
Now checks that $LISTEN is set
1996-10-18, by paulson
Defined pred using nat_case rather than nat_rec.
1996-10-16, by nipkow
corrected `correction` of o_assoc (of version 1.14),
1996-10-15, by oheimb
bound o_apply theorem to thy
1996-10-15, by oheimb
Removed extraneous spaces from all Makefiles
1996-10-15, by paulson
changed prettyprinting of ==>
1996-10-15, by paulson
Removed extraneous spaces from all Makefiles
1996-10-15, by paulson
Removed call to obsolete totalCPUTimer function
1996-10-14, by paulson
Addition of Sequents; removal of Modal and LK
1996-10-11, by paulson
Addition of OtwayRees_AN
1996-10-11, by paulson
Abadi and Needham's variant of Otway-Rees
1996-10-10, by paulson
Deleted obsolete clasets
1996-10-10, by paulson
Added comments describing better proofs
1996-10-10, by paulson
Simpset removes the de Morgan laws
1996-10-10, by paulson
Removed Modal since Sequents contains everything in it
1996-10-10, by paulson
Removed LK since Sequents contains everything in it
1996-10-10, by paulson
New root file with more description, and merging LK and Modal to Sequents
1996-10-10, by paulson
Tidied some proofs: changed needed for de Morgan laws
1996-10-10, by paulson
Addition of de Morgan laws
1996-10-10, by paulson
Removed Fast_tac made redundant by addition of de Morgan laws
1996-10-10, by paulson
Fuller description of examples
1996-10-09, by paulson
Plain text README files now redundant due to HTML versions
1996-10-09, by paulson
New version of axiom sees1_Says:
1996-10-09, by paulson
Plain text README files now redundant due to HTML versions
1996-10-09, by paulson
cond_timeit now catches exception Time, which sml/nj
1996-10-09, by paulson
Updated references
1996-10-09, by paulson
Added the de Morgan laws (incl quantifier versions) to basic simpset
1996-10-09, by paulson
New unified treatment of sequent calculi by Sara Kalvala
1996-10-09, by paulson
Put in the theorem Says_Crypt_not_lost
1996-10-08, by paulson
Put in a simpler and *much* faster proof of no_nonce_OR1_OR2
1996-10-08, by paulson
New guarantees for each line of protocol
1996-10-08, by paulson
Addition of Revl rule, and tidying
1996-10-08, by paulson
New theorem Crypt_imp_invKey_keysFor
1996-10-08, by paulson
Removed command made redundant by the new one-point rules
1996-10-08, by paulson
Introduction of Slow_tac and Slow_best_tac
1996-10-08, by paulson
Addition of one-point quantifier rewrite rules
1996-10-08, by paulson
Simple tidying
1996-10-07, by paulson
New proof required by change to simpdata.ML
1996-10-07, by paulson
Now replaces shorthand commands even if indented
1996-10-07, by paulson
New theorem Crypt_Fake_parts_insert
1996-10-07, by paulson
Simplified a proof
1996-10-07, by paulson
New comment in header
1996-10-07, by paulson
Tidied up some proofs
1996-10-07, by paulson
Ran expandshort
1996-10-07, by paulson
Removed commands made redundant by new one-point rules
1996-10-07, by paulson
Ran expandshort
1996-10-07, by paulson
New one-point rules for quantifiers
1996-10-07, by paulson
Greatly simplified the proof of A_can_trust
1996-10-01, by paulson
Working again with new theory Shared
1996-10-01, by paulson
Simplified main theorem by abstracting out newK
1996-10-01, by paulson
Moved sees_lost_agent_subset_sees_Spy to common file, and simplified main thm
1996-10-01, by paulson
Moved sees_lost_agent_subset_sees_Spy to common file
1996-10-01, by paulson
Added new guarantees for A and B
1996-10-01, by paulson
added shyps comment;
1996-10-01, by wenzelm
Inserted check for rewrite rules which introduce extra Vars on the rhs.
1996-09-30, by nipkow
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
1996-09-30, by paulson
Improved discussion of shyps thanks to Markus Wenzel
1996-09-30, by paulson
prune_params_tac no longer rewrites main goal
1996-09-30, by paulson
Added catch-all clause to drop, preventing exception Match
1996-09-26, by paulson
Now replaces uses of ssubst by stac
1996-09-26, by paulson
Documented sort hypotheses and improved discussion of derivations
1996-09-26, by paulson
Documented defer_tac and moved back the obsolete tactics like fold_tac
1996-09-26, by paulson
Documented stac, and updated the documentation of hyp_subst_tac
1996-09-26, by paulson
Declared stac
1996-09-26, by paulson
Ran expandshort; used stac instead of ssubst
1996-09-26, by paulson
Ran expandshort; used stac instead of ssubst
1996-09-26, by paulson
Ran expandshort; used stac instead of ssubst
1996-09-26, by paulson
Ran expandshort; used stac instead of ssubst
1996-09-26, by paulson
Introduction of "lost" argument
1996-09-26, by paulson
Ran expandshort
1996-09-26, by paulson
Changed freeze to freeze_thaw
1996-09-26, by paulson
Generalized freeze to freeze_thaw in order to
1996-09-26, by paulson
Last working version prior to addition of "lost" component
1996-09-26, by paulson
Last working version before "lost"
1996-09-25, by paulson
Last working version prior to introduction of "lost"
1996-09-25, by paulson
Prevention of Overflow exception (for SML/NJ) in gensym
1996-09-25, by paulson
Rationalized the rewriting of membership for {} and insert
1996-09-25, by paulson
Calls discgarb -c to realize dramatic space savings!
1996-09-25, by paulson
Fixed spelling error in comment
1996-09-24, by paulson
Added miniscoping for UN and INT
1996-09-24, by paulson
Restoration of reference to Nipkow, LICS, 1993
1996-09-24, by paulson
Moved Option out of IOA into core HOL
1996-09-24, by nipkow
Moved Option into core HOL which caused a few local changes.
1996-09-24, by nipkow
Proofs made more robust to work in presence of le_refl
1996-09-23, by paulson
Now uses init_html
1996-09-23, by paulson
Simplification of proof of unique_session_keys
1996-09-23, by paulson
Correction of protocol; addition of Reveal message; proofs of
1996-09-23, by paulson
Proof of Says_imp_old_keys is now more robust
1996-09-23, by paulson
Removal of the Notes constructor
1996-09-23, by paulson
New laws for messages
1996-09-23, by paulson
Simplification of definition of synth
1996-09-23, by paulson
Addition of le_refl to default simpset/claset
1996-09-23, by paulson
Removal of reference Nipkow-LICS-93
1996-09-23, by paulson
Proof of mult_le_mono is now more robust
1996-09-23, by paulson
New infix syntax: breaks line BEFORE operator
1996-09-23, by paulson
Optimized version of SELECT_GOAL, up to 10% faster
1996-09-23, by paulson
New operations on cterms. Now same names as in Logic
1996-09-23, by paulson
Addition of gensym
1996-09-23, by paulson
Bad version of Otway-Rees and the new attack on it
1996-09-23, by paulson
Reformatting; proved B_gets_secure_key
1996-09-13, by paulson
Abstraction of enemy_analz_tac over its argument
1996-09-13, by paulson
Reformatting
1996-09-13, by paulson
Reordering of premises for cut theorems, and new law MPair_synth_analz
1996-09-13, by paulson
No longer assumes Alice is not the Enemy in NS3.
1996-09-13, by paulson
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
1996-09-13, by paulson
Addition of Yahalom protocol
1996-09-13, by paulson
Removal of obsolete thm Fake_parts_insert
1996-09-13, by paulson
Addition of enemy_analz_tac and safe_solver
1996-09-13, by paulson
added flat_eq,
1996-09-12, by oheimb
renamed adm_disj_lemma11 to adm_lemma11
1996-09-12, by oheimb
added comment on is_flat
1996-09-12, by oheimb
added stric
1996-09-12, by oheimb
undo last revision
1996-09-12, by oheimb
bin/isa2latex: copy the binary to bin/isa2latex instead of linking it there
1996-09-12, by oheimb
new \subsubsection{Configuring conversion tables and keyboard bindings}
1996-09-12, by oheimb
Tidied many proofs, using AddIffs to let equivalences take
1996-09-12, by paulson
Installed AddIffs, and some code from HOL.ML
1996-09-12, by paulson
Simplification and tidying of definitions
1996-09-12, by paulson
Now hologic.ML is loaded in HOL.ML
1996-09-12, by paulson
New file cladata.ML
1996-09-12, by paulson
less
more
|
(0)
-1000
-120
+120
+1000
+3000
+10000
+30000
tip