| 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
|
| Tue, 07 Nov 2006 19:39:52 +0100 |
wenzelm |
theorem statements: incorporate Obtain.statement, tuned;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:46:48 +0100 |
wenzelm |
replaced const_syntax by notation, which operates on terms;
|
file |
diff |
annotate
|
| Sat, 14 Oct 2006 23:25:55 +0200 |
wenzelm |
added theorem(_i);
|
file |
diff |
annotate
|
| Mon, 09 Oct 2006 02:20:07 +0200 |
wenzelm |
added theorems(_i) -- with present_results;
|
file |
diff |
annotate
|
| Sat, 07 Oct 2006 01:31:18 +0200 |
wenzelm |
moved pretty_consts to proof_display.ML;
|
file |
diff |
annotate
|
| Fri, 29 Sep 2006 22:47:01 +0200 |
wenzelm |
Syntax.mode;
|
file |
diff |
annotate
|
| Tue, 16 May 2006 21:33:21 +0200 |
wenzelm |
added const_syntax(_i);
|
file |
diff |
annotate
|
| Sun, 07 May 2006 00:22:05 +0200 |
wenzelm |
removed 'concl is' patterns;
|
file |
diff |
annotate
|
| Tue, 02 May 2006 20:42:40 +0200 |
wenzelm |
abbreviation: observe local syntax mode;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2006 22:51:30 +0200 |
wenzelm |
abbreviation(_i): do not expand abbreviations, do not use derived_def;
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 18:26:04 +0100 |
wenzelm |
added abbreviation(_i);
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:59:54 +0100 |
wenzelm |
type local_theory;
|
file |
diff |
annotate
|
| Tue, 31 Jan 2006 18:19:36 +0100 |
wenzelm |
axiomatization: retrict parameters to occurrences in specs;
|
file |
diff |
annotate
|
| Sat, 28 Jan 2006 17:29:03 +0100 |
wenzelm |
added axiomatization_loc, definition_loc;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 19:03:16 +0100 |
wenzelm |
swapped Toplevel.theory_context;
|
file |
diff |
annotate
|
| Wed, 25 Jan 2006 00:21:44 +0100 |
wenzelm |
added definition(_i);
|
file |
diff |
annotate
|
| Tue, 24 Jan 2006 00:43:34 +0100 |
wenzelm |
renamed axiomatize(_i) to axiomatization(_i);
|
file |
diff |
annotate
|
| Sat, 21 Jan 2006 23:02:14 +0100 |
wenzelm |
simplified type attribute;
|
file |
diff |
annotate
|
| Fri, 13 Jan 2006 01:13:11 +0100 |
wenzelm |
uniform handling of fixes;
|
file |
diff |
annotate
|
| Tue, 10 Jan 2006 19:33:39 +0100 |
wenzelm |
generic attributes;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2006 23:28:01 +0100 |
wenzelm |
Theory specifications --- with type-inference, but no internal polymorphism.
|
file |
diff |
annotate
|