Sun, 07 Feb 2010 18:04:48 +0100 |
wenzelm |
simplified interface for ML antiquotations, struct_name is always "Isabelle";
|
file |
diff |
annotate
|
Sun, 15 Nov 2009 19:45:05 +0100 |
wenzelm |
eliminated obsolete thm position tags;
|
file |
diff |
annotate
|
Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
Wed, 04 Mar 2009 23:05:32 +0100 |
wenzelm |
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
|
file |
diff |
annotate
|
Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
Thu, 14 Aug 2008 16:52:56 +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
|
Thu, 10 Jul 2008 13:37:34 +0200 |
wenzelm |
@{lemma}: allow terminal method, close derivation unless (open) mode is given;
|
file |
diff |
annotate
|
Sat, 28 Jun 2008 22:52:07 +0200 |
wenzelm |
Isar theorem values within ML.
|
file |
diff |
annotate
|