| Mon, 22 Mar 2010 19:25:14 +0100 |
wenzelm |
use Specification.axiom, together with Drule.export_without_context that was implicit in the former PureThy.add_axioms (cf. f81557a124d5);
|
changeset |
files
|
| Mon, 22 Mar 2010 19:23:03 +0100 |
wenzelm |
added Specification.axiom convenience;
|
changeset |
files
|
| Mon, 22 Mar 2010 15:07:07 +0100 |
blanchet |
detect OFCLASS() axioms in Nitpick;
|
changeset |
files
|
| Mon, 22 Mar 2010 13:48:15 +0100 |
bulwahn |
merged
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
contextifying the compilation of the predicate compiler
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
removed unused Predicate_Compile_Set
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
avoiding fishing for split_asm rule in the predicate compiler
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
contextifying the proof procedure in the predicate compiler
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
making flat triples to nested tuple to remove general triple functions
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
reduced the debug output functions from 2 to 1
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
some improvements thanks to Makarius source code review
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
enabling a previously broken example of the predicate compiler again
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
improving handling of case expressions in predicate rewriting
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
adding depth_limited_random compilation to predicate compiler
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
a new simpler random compilation for the predicate compiler
|
changeset |
files
|