| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
|
changeset |
files
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
dummy implementation
|
changeset |
files
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
split relevance filter code into three files
|
changeset |
files
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
optimized type intersection, hoping this will reduce the number of sudden Interrupts in the "incr_tvar" code
|
changeset |
files
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
add Isabelle dependencies to tweak relevance filter
|
changeset |
files
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
generate ATP dependencies
|
changeset |
files
|
| Wed, 11 Jul 2012 13:59:39 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Wed, 11 Jul 2012 13:54:37 +0200 |
bulwahn |
adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
|
changeset |
files
|
| Wed, 11 Jul 2012 11:28:27 +0200 |
blanchet |
comment
|
changeset |
files
|
| Wed, 11 Jul 2012 11:28:10 +0200 |
blanchet |
nicer output
|
changeset |
files
|
| Wed, 11 Jul 2012 09:32:29 +0200 |
blanchet |
rationalized output
|
changeset |
files
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
generate Meng--Paulson facts for evaluation purposes
|
changeset |
files
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
export useful functions
|
changeset |
files
|