| Wed, 25 Mar 2009 21:35:49 +0100 |
wenzelm |
@{binding} is not a constructor term and should not be inlined, otherwise we loose value polymorphism;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2009 15:59:43 +0100 |
wenzelm |
ML_Syntax.make_binding;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 21:25:15 +0100 |
wenzelm |
eliminated type Args.T;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 17:26:14 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 21:49:05 +0100 |
wenzelm |
added @{binding} ML antiquotations;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Fri, 15 Aug 2008 15:50:44 +0200 |
wenzelm |
Args.name_source(_position) for proper position information;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 16:52:54 +0200 |
wenzelm |
ML_Context.add_antiq: pass position;
|
file |
diff |
annotate
|
| Sat, 09 Aug 2008 22:43:46 +0200 |
wenzelm |
unified Args.T with OuterLex.token, renamed some operations;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2008 22:52:11 +0200 |
wenzelm |
moved theorem values to ml_thms.ML;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2008 15:17:28 +0200 |
wenzelm |
added macro interface;
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 15:06:25 +0200 |
wenzelm |
Args.context;
|
file |
diff |
annotate
|
| Wed, 25 Jun 2008 17:38:39 +0200 |
wenzelm |
re-use official outer keywords;
|
file |
diff |
annotate
|
| Tue, 24 Jun 2008 19:43:16 +0200 |
wenzelm |
Common ML antiquotations.
|
file |
diff |
annotate
|