| Thu, 14 Dec 2006 15:31:22 +0100 |
wenzelm |
defs/notes: more robust transitivity reasoning;
|
file |
diff |
annotate
|
| Wed, 13 Dec 2006 15:47:36 +0100 |
wenzelm |
internal_abbrev: observe print mode;
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 21:25:14 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 20:49:31 +0100 |
wenzelm |
removed is_class -- handled internally;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 22:27:03 +0100 |
wenzelm |
defs: increased entropy of mixfix handling;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 17:37:55 +0100 |
wenzelm |
removed junk;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 15:30:46 +0100 |
wenzelm |
added is_class (approximation);
|
file |
diff |
annotate
|
| Sat, 09 Dec 2006 18:05:37 +0100 |
wenzelm |
TermSyntax.abbrev;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 23:16:55 +0100 |
wenzelm |
reorganized structure Tactic vs. MetaSimplifier;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 17:58:39 +0100 |
wenzelm |
TermSyntax.notation/abbrevs;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 22:14:53 +0100 |
wenzelm |
target_name: allow qualified names;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 00:29:16 +0100 |
wenzelm |
notes: added non-official name;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 17:42:23 +0100 |
wenzelm |
notes: proper naming of thm proof, activated import_export_proof;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 16:48:42 +0100 |
wenzelm |
notes: more careful treatment of Goal.close_result;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 14:17:37 +0100 |
wenzelm |
notes: proper import/export of proofs (still inactive);
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 15:45:02 +0100 |
wenzelm |
reworked notes: towards proper import/export of proof terms;
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 04:11:18 +0100 |
wenzelm |
Assumption.assms_of: cterm;
|
file |
diff |
annotate
|
| Tue, 28 Nov 2006 00:35:27 +0100 |
wenzelm |
simplified '?' operator;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2006 18:07:31 +0100 |
wenzelm |
simplified consts: no auxiliary params, sane mixfix syntax;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 20:33:37 +0100 |
wenzelm |
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
|
file |
diff |
annotate
|
| Wed, 22 Nov 2006 17:38:36 +0100 |
wenzelm |
consts: ProofContext.set_stmt true -- avoids naming of local thms;
|
file |
diff |
annotate
|
| Tue, 21 Nov 2006 18:07:29 +0100 |
wenzelm |
LocalTheory.axioms/notes/defs: proper kind;
|
file |
diff |
annotate
|
| Fri, 10 Nov 2006 22:18:53 +0100 |
wenzelm |
removed mapping;
|
file |
diff |
annotate
|
| Thu, 09 Nov 2006 21:44:34 +0100 |
wenzelm |
init: '-' refers to global context;
|
file |
diff |
annotate
|
| Sat, 14 Oct 2006 23:25:56 +0200 |
wenzelm |
added peek;
|
file |
diff |
annotate
|
| Thu, 12 Oct 2006 22:57:42 +0200 |
wenzelm |
added peek;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2006 22:55:21 +0200 |
wenzelm |
exit: pass interactive flag;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2006 00:27:37 +0200 |
wenzelm |
added begin;
|
file |
diff |
annotate
|
| Mon, 09 Oct 2006 02:20:08 +0200 |
wenzelm |
added exit;
|
file |
diff |
annotate
|
| Sat, 07 Oct 2006 01:31:23 +0200 |
wenzelm |
Common theory targets.
|
file |
diff |
annotate
|