| Thu, 10 Jul 2008 13:37:35 +0200 |
wenzelm |
@{lemma}: allow terminal method;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2008 21:21:13 +0200 |
wenzelm |
@{lemma}: 'by' keyword;
|
file |
diff |
annotate
|
| Tue, 24 Jun 2008 19:43:20 +0200 |
wenzelm |
Antiquote.Open/Close;
|
file |
diff |
annotate
|
| Wed, 18 Jun 2008 18:55:06 +0200 |
wenzelm |
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
|
file |
diff |
annotate
|
| Mon, 26 May 2008 17:55:37 +0200 |
haftmann |
proper lemma [source] antiquotation
|
file |
diff |
annotate
|
| Wed, 14 May 2008 20:30:53 +0200 |
wenzelm |
added defined_command, defined_option;
|
file |
diff |
annotate
|
| Tue, 29 Apr 2008 19:55:02 +0200 |
haftmann |
added lemma antiquotation
|
file |
diff |
annotate
|
| Thu, 17 Apr 2008 22:22:19 +0200 |
wenzelm |
pretty_term: no revert_skolems here, but auto_fixes (token translations will do the rest);
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 00:02:54 +0100 |
wenzelm |
reorganized signature of ML_Context;
|
file |
diff |
annotate
|
| Mon, 24 Mar 2008 23:34:24 +0100 |
wenzelm |
ML runtime compilation: pass position, tuned signature;
|
file |
diff |
annotate
|
| Sun, 11 Nov 2007 20:29:07 +0100 |
wenzelm |
abbrev: bypass full term check via ProofContext.standard_infer_types (prevents forced expansion);
|
file |
diff |
annotate
|
| Sat, 10 Nov 2007 14:31:23 +0100 |
wenzelm |
@{const}: improved ProofContext.read_const does the job;
|
file |
diff |
annotate
|
| Tue, 30 Oct 2007 14:39:37 +0100 |
haftmann |
const antiquotation clarified
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 17:06:20 +0200 |
wenzelm |
tuned Const.the_abbreviation;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 00:20:13 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| Sun, 23 Sep 2007 22:23:27 +0200 |
wenzelm |
TypeInfer.constrain: canonical argument order;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 19:45:49 +0200 |
wenzelm |
marked some CRITICAL sections;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 16:45:03 +0200 |
wenzelm |
PrintMode.with_modes;
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 23:18:48 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 23:29:52 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 22:46:59 +0200 |
wenzelm |
print_antiquotations: sort_strings;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:10:35 +0100 |
wenzelm |
renamed Isar/isar_output.ML to Thy/thy_output.ML;
|
file |
diff |
annotate
|