| Tue, 02 Sep 2008 22:41:36 +0200 |
wenzelm |
* Generic Toplevel.add_hook interface allows to analyze the result of
|
changeset |
files
|
| Tue, 02 Sep 2008 22:37:20 +0200 |
nipkow |
Replaced Library/NatPair by Nat_Int_Bij.
|
changeset |
files
|
| Tue, 02 Sep 2008 22:20:27 +0200 |
wenzelm |
added new_thms_deps (operates on global facts, some name_hint approximation);
|
changeset |
files
|
| Tue, 02 Sep 2008 22:20:25 +0200 |
wenzelm |
theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;
|
changeset |
files
|
| Tue, 02 Sep 2008 22:20:24 +0200 |
wenzelm |
added add_hook interface for post-transition hooks;
|
changeset |
files
|
| Tue, 02 Sep 2008 22:20:21 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 02 Sep 2008 22:20:20 +0200 |
wenzelm |
ProofDisplay.print_results;
|
changeset |
files
|
| Tue, 02 Sep 2008 22:20:16 +0200 |
wenzelm |
no pervasive bindings;
|
changeset |
files
|
| Tue, 02 Sep 2008 21:31:28 +0200 |
nipkow |
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
|
changeset |
files
|
| Tue, 02 Sep 2008 20:38:17 +0200 |
haftmann |
distributed literal code generation out of central infrastructure
|
changeset |
files
|
| Tue, 02 Sep 2008 20:07:51 +0200 |
wenzelm |
* Result facts now refer to the *full* internal name;
|
changeset |
files
|
| Tue, 02 Sep 2008 20:04:26 +0200 |
wenzelm |
* Name bindings in higher specification mechanisms;
|
changeset |
files
|
| Tue, 02 Sep 2008 18:01:24 +0200 |
wenzelm |
pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
|
changeset |
files
|
| Tue, 02 Sep 2008 18:01:23 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Tue, 02 Sep 2008 17:31:20 +0200 |
ballarin |
Interpretation commands no longer accept interpretation attributes.
|
changeset |
files
|