isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

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

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

isabelle