| Thu, 11 Oct 2007 21:10:42 +0200 |
wenzelm |
removed unused/impure quiet_mode;
|
file |
diff |
annotate
|
| Wed, 10 Oct 2007 17:31:56 +0200 |
wenzelm |
generalized notation interface (add or del);
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 17:10:36 +0200 |
wenzelm |
Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 20:29:24 +0200 |
wenzelm |
replaced literal 'a by Name.aT;
|
file |
diff |
annotate
|
| Wed, 26 Sep 2007 22:21:02 +0200 |
wenzelm |
read/check_specification: free_dummy_patterns;
|
file |
diff |
annotate
|
| Wed, 26 Sep 2007 19:17:59 +0200 |
wenzelm |
read/check_specification: proper type inference across multiple sections, result is in closed form;
|
file |
diff |
annotate
|
| Sat, 22 Sep 2007 17:45:58 +0200 |
wenzelm |
ProofContext.mode_abbrev;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 07:36:15 +0200 |
haftmann |
distinction between regular and default code theorems
|
file |
diff |
annotate
|
| Fri, 07 Sep 2007 22:13:49 +0200 |
wenzelm |
theorem: apply hook last;
|
file |
diff |
annotate
|
| Thu, 06 Sep 2007 12:30:11 +0200 |
wenzelm |
theorem hooks: apply in declaration order;
|
file |
diff |
annotate
|
| Tue, 28 Aug 2007 19:45:45 +0200 |
wenzelm |
TheoremHook: fixed copy-paste mistake;
|
file |
diff |
annotate
|
| Tue, 28 Aug 2007 18:03:16 +0200 |
berghofe |
- theorem(_i) now also takes "interactive" flag as argument
|
file |
diff |
annotate
|
| Fri, 10 Aug 2007 17:04:34 +0200 |
haftmann |
new structure for code generator modules
|
file |
diff |
annotate
|
| Thu, 10 May 2007 15:50:28 +0200 |
berghofe |
Changed name of raw definition.
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 11:21:42 +0200 |
haftmann |
Isar definitions are now added explicitly to code theorem table
|
file |
diff |
annotate
|
| Fri, 15 Dec 2006 00:08:15 +0100 |
wenzelm |
renamed LocalTheory.assert to affirm;
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 20:49:19 +0100 |
wenzelm |
LocalTheory.abbrev;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 15:30:45 +0100 |
wenzelm |
LocalTheory.notation/abbrev;
|
file |
diff |
annotate
|
| Sat, 09 Dec 2006 18:05:49 +0100 |
wenzelm |
TermSyntax.abbrev;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 21:08:50 +0100 |
wenzelm |
definition/abbreviation: single argument;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 17:58:39 +0100 |
wenzelm |
TermSyntax.notation/abbrevs;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 22:14:42 +0100 |
wenzelm |
Attrib.internal: morphism;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 14:17:25 +0100 |
wenzelm |
Goal.norm/close_result;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2006 18:07:29 +0100 |
wenzelm |
abbrevs: no result;
|
file |
diff |
annotate
|
| Tue, 21 Nov 2006 20:48:11 +0100 |
wenzelm |
theorem(_i): note assms of statement;
|
file |
diff |
annotate
|
| Tue, 21 Nov 2006 18:07:31 +0100 |
wenzelm |
LocalTheory.axioms/notes/defs: proper kind;
|
file |
diff |
annotate
|
| Tue, 14 Nov 2006 22:17:01 +0100 |
wenzelm |
replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
|
file |
diff |
annotate
|
| Tue, 14 Nov 2006 15:29:52 +0100 |
wenzelm |
simplified Proof.theorem(_i) interface;
|
file |
diff |
annotate
|
| Thu, 09 Nov 2006 21:44:33 +0100 |
wenzelm |
abbrevs: return result;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 21:30:03 +0100 |
wenzelm |
complex goal statements: misc cleanup;
|
file |
diff |
annotate
|