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.
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
1996-09-11, by nipkow
Removed refs to clasets like rel_cs etc. Used implicit claset.
1996-09-11, by nipkow
Converted proofs to use default clasets.
1996-09-10, by nipkow
Added Auth to the test target
1996-09-10, by paulson
Now runs all Auth proofs
1996-09-10, by paulson
Now uses DB-ROOT.ML, which is separate from ROOT.ML
1996-09-10, by paulson
Dedicated root file for making the Auth database
1996-09-10, by paulson
Beefed-up auto-tactic: now repeatedly simplifies if needed
1996-09-10, by paulson
"bad" set simplifies statements of many theorems
1996-09-09, by paulson
added cterm_lift_inst_rule
1996-09-09, by nipkow
Stronger proofs; work for Otway-Rees
1996-09-09, by paulson
Stronger proofs; work for Otway-Rees
1996-09-09, by paulson
These simpsets must not use miniscoping
1996-09-09, by paulson
Corrected associativity: must be to right, as the type dictatess
1996-09-09, by paulson
Removal of (EX x. P) <-> P and (ALL x. P) <-> P
1996-09-09, by paulson
Improved error handling: if there are syntax or type-checking
1996-09-06, by paulson
Modified proof to work with miniscoping
1996-09-06, by paulson
Now uses thin_tac
1996-09-05, by paulson
Now uses thin_tac
1996-09-05, by paulson
Renaming of _rews to _simps
1996-09-05, by paulson
Added thin_tac to signature; previous change was useless
1996-09-05, by paulson
Some renaming. Note that this miniscoping is more
1996-09-05, by paulson
Introduction of miniscoping for FOL
1996-09-05, by paulson
Pretty-printing change to emphasize the scope of assumptions
1996-09-05, by paulson
Declared thin_tac
1996-09-05, by paulson
Miniscoping rules are deleted, as these brittle proofs
1996-09-05, by paulson
Simplified some proofs for compatibility with miniscoping
1996-09-05, by paulson
Added miniscoping to the simplifier: quantifiers are now pushed in
1996-09-05, by paulson
Fixed pretty-printing of {|...|}
1996-09-03, by paulson
New theorems for Fake case
1996-09-03, by paulson
A further tidying
1996-09-03, by paulson
ROOT file for Auth directory
1996-09-03, by paulson
Renaming and simplification
1996-09-03, by paulson
Renaming and simplification
1996-09-03, by paulson
Initial working proof of Otway-Rees protocol
1996-09-03, by paulson
Swaped two conditions in the completeness statement.
1996-08-23, by nipkow
Generalized my_lemma1: (c3,s3) |--> cs3
1996-08-23, by nipkow
Now deepen_tac can take advantage of wrappers --
1996-08-22, by paulson
Proved mem_if
1996-08-22, by paulson
Proved set_of_list_subset_Cons
1996-08-22, by paulson
For building the security theory as a separate database
1996-08-22, by paulson
Separation of theory Event into two parts:
1996-08-21, by paulson
Addition of message NS5
1996-08-21, by paulson
Tidying: removing redundant args in classical reasoner calls
1996-08-21, by paulson
Added le_eq_less_Suc; fixed some comments;
1996-08-21, by paulson
Working version of NS, messages 1-4!
1996-08-20, by paulson
Working version of NS, messages 1-3, WITH INTERLEAVING
1996-08-20, by paulson
Added ref to allow suppression of error msgs
1996-08-20, by paulson
New classical reasoner: warns of, and ignores, redundant rules.
1996-08-20, by paulson
Addition of function set_of_list
1996-08-20, by paulson
Some tidying. This brittle proof depends upon
1996-08-20, by paulson
Corrected for new classical reasoner: redundant rules
1996-08-20, by paulson
updated html-link
1996-08-19, by nipkow
Installation of auto_tac; re-organization
1996-08-19, by paulson
Tidied up the proofs
1996-08-19, by paulson
Added impOfSubs
1996-08-19, by paulson
Now less_zeroE is a Safe Elim rule
1996-08-19, by paulson
Improved comment
1996-08-19, by paulson
Added proof of Un_insert_right
1996-08-19, by paulson
Changed precedences to remove ambiguities in r^+ notation
1996-08-19, by paulson
less
more
|
(0)
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip