Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-1000
-300
-100
-96
+96
+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.
Tidied up a big mess in UN_parts_sees_Says
1996-10-28, by paulson
Changing from the Reveal to the Oops rule
1996-10-28, by paulson
Simplifid proofs.
1996-10-27, by nipkow
Added (? x. t=x) = True
1996-10-25, by nipkow
Documents the use of negative arguments to choplev and prlev
1996-10-24, by paulson
Changed comment to illustrate use of pathname
1996-10-24, by paulson
Allowing negative levels (as offsets) in prlev and choplev
1996-10-24, by paulson
New Oops message, with Server as source to ensure
1996-10-24, by paulson
New theorem Crypt_Spy_analz_lost; improvements to spy_analz_tac; ex_strip_tac
1996-10-24, by paulson
Two new protocol variants
1996-10-24, by paulson
Moved ex_strip_tac to the common part
1996-10-24, by paulson
Removal of unused predicate isSpy
1996-10-24, by paulson
Handles pathnames in ISABELLECOMP
1996-10-24, by paulson
Mentions the possibility of pathnames in ISABELLECOMP;
1996-10-21, by paulson
Creates a bigger main window
1996-10-21, by paulson
ISABELLECOMP may now have a leading pathname
1996-10-21, by paulson
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
1996-10-21, by nipkow
Added trans_tac (see Provers/nat_transitive.ML)
1996-10-21, by nipkow
Solves simple arithmetic goals.
1996-10-21, by nipkow
Subst as modified by Konrad Slind
1996-10-18, by paulson
Konrad Slind's TFL
1996-10-18, by paulson
New version of Yahalom, as recommended on p 259 of BAN paper
1996-10-18, by paulson
Addition of Reveal message
1996-10-18, by paulson
Deleted obsolete rewrites (they are now in HOL/simpdata)
1996-10-18, by paulson
Reveal -> Revl
1996-10-18, by paulson
The new proof of the lemma for new_nonces_not_seen is faster
1996-10-18, by paulson
Generaly tidying up
1996-10-18, by paulson
Important correction to comment
1996-10-18, by paulson
Replaced excluded_middle_tac by case_tac; tidied proofs
1996-10-18, by paulson
Tidied up the proof of A_trust_NS4
1996-10-18, by paulson
Replaced excluded_middle_tac by case_tac
1996-10-18, by paulson
Moving the CPUtimer declaration into cond_timeit should
1996-10-18, by paulson
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
less
more
|
(0)
-1000
-300
-100
-96
+96
+100
+300
+1000
+3000
+10000
+30000
tip