| Thu, 06 Jul 2006 12:18:17 +0200 |
paulson |
some tidying; fixed the output of theorem names
|
changeset |
files
|
| Thu, 06 Jul 2006 11:26:49 +0200 |
wenzelm |
def_export: Drule.generalize;
|
changeset |
files
|
| Thu, 06 Jul 2006 11:26:46 +0200 |
wenzelm |
matchers: fall back on plain first_order_matchers, not pattern;
|
changeset |
files
|
| Wed, 05 Jul 2006 23:51:22 +0200 |
kleing |
make sure $DISTPREFIX exists before calling makedist
|
changeset |
files
|
| Wed, 05 Jul 2006 16:24:28 +0200 |
paulson |
removed the "tagging" feature
|
changeset |
files
|
| Wed, 05 Jul 2006 16:24:10 +0200 |
paulson |
made the conversion of elimination rules more robust
|
changeset |
files
|
| Wed, 05 Jul 2006 14:22:09 +0200 |
mengj |
Literals aren't sorted any more.
|
changeset |
files
|
| Wed, 05 Jul 2006 14:21:22 +0200 |
mengj |
Literals aren't sorted any more. Output overloaded constants' type var instantiations.
|
changeset |
files
|
| Wed, 05 Jul 2006 11:32:38 +0200 |
schirmer |
fixed let-simproc
|
changeset |
files
|
| Tue, 04 Jul 2006 21:26:26 +0200 |
wenzelm |
Isar: 'print_facts' prints all local facts;
|
changeset |
files
|
| Tue, 04 Jul 2006 21:22:53 +0200 |
wenzelm |
print_lthms: include unnamed facts from index;
|
changeset |
files
|
| Tue, 04 Jul 2006 21:22:52 +0200 |
wenzelm |
added content;
|
changeset |
files
|
| Tue, 04 Jul 2006 21:22:51 +0200 |
wenzelm |
added props selector;
|
changeset |
files
|
| Tue, 04 Jul 2006 21:22:50 +0200 |
wenzelm |
print_facts: all facts;
|
changeset |
files
|
| Tue, 04 Jul 2006 19:49:59 +0200 |
wenzelm |
add_abbrevs/polymorphic: Variable.exportT_terms avoids over-generalization;
|
changeset |
files
|
| Tue, 04 Jul 2006 19:49:58 +0200 |
wenzelm |
instantiate_tfrees: Thm.generalize;
|
changeset |
files
|
| Tue, 04 Jul 2006 19:49:57 +0200 |
wenzelm |
removed parrot comment;
|
changeset |
files
|
| Tue, 04 Jul 2006 19:49:56 +0200 |
wenzelm |
Proof by guessing.
|
changeset |
files
|
| Tue, 04 Jul 2006 19:49:55 +0200 |
wenzelm |
guess: proper context for polymorphic parameters;
|
changeset |
files
|
| Tue, 04 Jul 2006 19:49:54 +0200 |
wenzelm |
polymorphic: always generalize wrt. used_types;
|
changeset |
files
|
| Tue, 04 Jul 2006 19:49:53 +0200 |
wenzelm |
varifyT: no longer pervasive;
|
changeset |
files
|
| Tue, 04 Jul 2006 19:49:52 +0200 |
wenzelm |
added generalize/instantiate_option;
|
changeset |
files
|
| Tue, 04 Jul 2006 19:49:51 +0200 |
wenzelm |
added map_proof_terms_option;
|
changeset |
files
|
| Tue, 04 Jul 2006 19:49:50 +0200 |
wenzelm |
added generalize;
|
changeset |
files
|
| Tue, 04 Jul 2006 19:49:49 +0200 |
wenzelm |
Thm.varifyT;
|
changeset |
files
|
| Tue, 04 Jul 2006 19:49:47 +0200 |
wenzelm |
added ex/Guess.thy;
|
changeset |
files
|
| Tue, 04 Jul 2006 18:39:59 +0200 |
wenzelm |
skip_proofs: do not skip proofs of schematic goals (warning);
|
changeset |
files
|
| Tue, 04 Jul 2006 18:39:58 +0200 |
wenzelm |
added schematic_goal;
|
changeset |
files
|
| Tue, 04 Jul 2006 18:39:57 +0200 |
wenzelm |
added 'unfolding';
|
changeset |
files
|
| Tue, 04 Jul 2006 17:26:02 +0200 |
urbanc |
added simplification rules to the fresh_guess tactic
|
changeset |
files
|