| Sat, 24 Jul 2010 21:22:21 +0200 |
wenzelm |
moved basic thy file name operations from Thy_Load to Thy_Header;
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Thu, 17 Jun 2010 15:59:46 +0200 |
haftmann |
explicit type variable arguments for constructors
|
file |
diff |
annotate
|
| Tue, 15 Jun 2010 08:32:32 +0200 |
haftmann |
formal introduction of case cong
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Sun, 30 May 2010 21:34:19 +0200 |
wenzelm |
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 15:00:42 +0200 |
haftmann |
dropped code_datatype antiquotation
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 16:56:18 +0200 |
haftmann |
take into account tupled constructors
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 15:17:09 +0200 |
haftmann |
added code_reflect command
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 15:20:57 +0200 |
haftmann |
optionally ignore errors during translation of equations
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 22:06:43 +0100 |
wenzelm |
clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 11:10:20 +0100 |
haftmann |
proper distinction of code datatypes and abstypes
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 11:06:22 +0100 |
haftmann |
context theorem is optional
|
file |
diff |
annotate
|
| Sun, 07 Feb 2010 18:04:48 +0100 |
wenzelm |
simplified interface for ML antiquotations, struct_name is always "Isabelle";
|
file |
diff |
annotate
|
| Tue, 08 Dec 2009 14:31:19 +0100 |
haftmann |
simplified notion of empty module name
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 16:27:48 +0100 |
haftmann |
split off evaluation mechanisms in separte module Code_Eval
|
file |
diff |
annotate
| base
|