| Fri, 01 Aug 2014 23:29:50 +0200 |
blanchet |
fine-tuned Isar reconstruction, esp. boolean simplifications
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 23:29:49 +0200 |
blanchet |
centralized boolean simplification so that e.g. LEO-II benefits from it
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tuned order of arguments
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
more rational unskolemizing of names
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
remove lambda-lifting related assumptions from generated Isar proofs
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:13 +0200 |
fleury |
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:13 +0200 |
fleury |
imported patch satallax_skolemization_in_tree_part
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
veriT changes for lifted terms, and ite_elim rules.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
Subproofs for the SMT solver veriT.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
Basic support for the SMT prover veriT.
|
file |
diff |
annotate
|