Mercurial
Mercurial
>
repos
>
isabelle
/ shortlog
summary
| shortlog |
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
(0)
-30000
-10000
-3000
-1000
-300
-100
-30
-10
-8
+8
+10
+30
+100
+300
+1000
+3000
+10000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
Tue, 30 Sep 2014 16:01:46 +0200
blanchet
proper types for applied variables, for typed formats (TFF0, DFG)
changeset
|
files
Tue, 30 Sep 2014 15:18:01 +0200
blanchet
don't affect other subgoals with 'auto' in one-liner proofs
changeset
|
files
Tue, 30 Sep 2014 14:54:14 +0200
blanchet
tuned output in case of one-liner failure
changeset
|
files
Tue, 30 Sep 2014 14:40:48 +0200
blanchet
updated docs with two provers: veriT and Zipperposition
changeset
|
files
Tue, 30 Sep 2014 14:19:25 +0200
blanchet
give more facts to veriT -- it seems to be able to cope with them
changeset
|
files
Tue, 30 Sep 2014 14:18:07 +0200
blanchet
use native encoding with Vampire -- modern versions handle types better than the old ones
changeset
|
files
Tue, 30 Sep 2014 14:18:07 +0200
blanchet
always minimize, to reinvoke the prover with nicer options and yield a nicer Isar proof (potentially -- cf. 'full_proof')
changeset
|
files
Tue, 30 Sep 2014 14:01:33 +0200
fleury
correct inlining in veriT's subproofs.
changeset
|
files
(0)
-30000
-10000
-3000
-1000
-300
-100
-30
-10
-8
+8
+10
+30
+100
+300
+1000
+3000
+10000
tip