Mercurial
Mercurial
>
repos
>
testboard
/ 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
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
Defines KeyWithNonce, which is used to prove the secrecy of NB
19970618, by paulson
Addition of not_imp (which pushes negation into implication) as a default
19970618, by paulson
Corrected Title in header lines
19970618, by paulson
Streamlined proofs of the secrecy of NB and added authentication of A and B
19970618, by paulson
Removed Says_Crypt_lost and Says_Crypt_not_lost.
19970618, by paulson
Removed Says_Crypt_lost and Says_Crypt_not_lost.
19970618, by paulson
Adapted proofs to the removal of Says_Crypt_lost and Says_Crypt_not_lost
19970618, by paulson
Deleted spurious reference to Spy_not_see_NB, which by chance was defined
19970618, by paulson
converse > ^1
19970617, by nipkow
Type constraint added to ensure that "length" refers to lists. Maybe should
19970616, by paulson
Replacing the primrec definition of "length" by a translation to the builtin
19970616, by paulson
Tuned wf_iff_no_infinite_down_chain proof, based on Konrads ideas.
19970613, by nipkow
changed compatible definition;
19970613, by mueller
added deadlock
19970612, by mueller
added deadlock freedom, polished definitions and proofs
19970612, by mueller
Strengthened and streamlined the Yahalom proofs
19970609, by paulson
Useful new lemma
19970609, by paulson
eliminated nonASCII;
19970606, by wenzelm
Added
19970606, by nipkow
improved function 'nonreserved'
19970606, by oheimb
Removed a few redundant additions of simprules or classical rules
19970606, by paulson
The name bex_conj_distrib was WRONG
19970606, by paulson
Better miniscoping for bounded quantifiers
19970606, by paulson
Tidying and simplification of declarations
19970606, by paulson
Much polishing of proofs
19970606, by paulson
New miniscoping rules for ALL
19970606, by paulson
New facts about In0/1 by Burkhart Wolff
19970606, by paulson
New miniscoping rules ball_triv and bex_triv
19970606, by paulson
Mended the definition of ack(0,n)
19970606, by paulson
Two new examples; corrected a comment
19970606, by paulson
New example theory: Recdef
19970606, by paulson
added finite_converse
19970605, by nipkow
Moved image_is_empty from Finite.ML to equalities.ML
19970605, by nipkow
Modified a few defs and proofs because of the changes to theory Finite.thy.
19970605, by nipkow
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
19970605, by nipkow
New recdef examples
19970605, by paulson
Removal of freeze_vars and thaw_vars. New freeze_thaw
19970605, by paulson
freezeT now refers to Type.freeze_thaw
19970605, by paulson
Tidying of signature. More robust renaming in freeze_thaw.
19970605, by paulson
Removal of freeze_vars and thaw_vars (quite unused...)
19970605, by paulson
Removal of radixstring from string_of_int; addition of string_of_indexname
19970605, by paulson
There was never need for another copy of radixstring...
19970605, by paulson
Numerous simplifications and removal of HOLisms
19970605, by paulson
Now loads theory Recdef
19970605, by paulson
A slight simplification of optstring
19970605, by paulson
Now extracts the predicate variable from induct0 insteead of trying to
19970605, by paulson
Deleted the obsolete "pred_list" relation
19970605, by paulson
Documented the new distinct_subgoals_tac
19970605, by paulson
A slight simplification of optstring
19970605, by paulson
Now extracts the predicate variable from induct0 insteead of trying to
19970605, by paulson
Made the pseudotype of split_rule_var a separate argument
19970605, by paulson
eliminated nonASCII;
19970604, by wenzelm
eliminated freeze_vars;
19970604, by wenzelm
changed priority of > from [6,5]5 to [1,0]0
19970604, by mueller
is_blank: fixed space2;
19970603, by wenzelm
No longer refers to internal TFL structures
19970603, by paulson
More deHOLification: using Free, Const, etc. instead of mk_var, mk_const
19970603, by paulson
New theory "Power" of exponentiation (and binomial coefficients)
19970603, by paulson
New theorem about the cardinality of the powerset (uses exponentiation)
19970603, by paulson
Type inference makes a Const here, perhaps elsewhere?thry.sml
19970602, by paulson
less
more

(0)
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip