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
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.
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
less
more
|
(0)
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip