| Sun, 30 May 2010 21:34:19 +0200 |
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 |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file | diff | annotate |
| Mon, 03 May 2010 14:25:56 +0200 |
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 |
dropped code_datatype antiquotation
|
file | diff | annotate |
| Wed, 28 Apr 2010 16:56:18 +0200 |
take into account tupled constructors
|
file | diff | annotate |
| Wed, 28 Apr 2010 15:17:09 +0200 |
added code_reflect command
|
file | diff | annotate |
| Wed, 21 Apr 2010 15:20:57 +0200 |
optionally ignore errors during translation of equations
|
file | diff | annotate |
| Thu, 25 Feb 2010 22:06:43 +0100 |
clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
|
file | diff | annotate |
| Mon, 22 Feb 2010 11:10:20 +0100 |
proper distinction of code datatypes and abstypes
|
file | diff | annotate |
| Fri, 19 Feb 2010 11:06:22 +0100 |
context theorem is optional
|
file | diff | annotate |
| Sun, 07 Feb 2010 18:04:48 +0100 |
simplified interface for ML antiquotations, struct_name is always "Isabelle";
|
file | diff | annotate |
| Tue, 08 Dec 2009 14:31:19 +0100 |
simplified notion of empty module name
|
file | diff | annotate |
| Mon, 07 Dec 2009 16:27:48 +0100 |
split off evaluation mechanisms in separte module Code_Eval
|
file | diff | annotate | base |