src/Pure/ML/ml_antiquote.ML
Wed, 21 Jul 2010 15:02:51 +0200 wenzelm ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
Thu, 03 Jun 2010 22:06:37 +0200 wenzelm allow qualified names;
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
Sat, 15 May 2010 23:16:32 +0200 wenzelm refer directly to structure Keyword and Parse;
Fri, 16 Apr 2010 10:52:10 +0200 wenzelm added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
Tue, 09 Mar 2010 14:36:41 +0100 wenzelm ProofContext.read_class/read_type_name_proper;
Wed, 03 Mar 2010 00:28:22 +0100 wenzelm authentic syntax for classes and type constructors;
Sat, 27 Feb 2010 20:56:03 +0100 wenzelm clarified @{const_name} (only logical consts) vs. @{const_abbrev};
Sat, 27 Feb 2010 13:32:38 +0100 wenzelm ML antiquotations for type classes;
Thu, 25 Feb 2010 22:08:43 +0100 wenzelm more orthogonal antiquotations for type constructors;
Sun, 21 Feb 2010 22:35:02 +0100 wenzelm slightly more abstract syntax mark/unmark operations;
Sun, 21 Feb 2010 21:08:25 +0100 wenzelm authentic syntax for *all* term constants;
Tue, 16 Feb 2010 11:27:29 +0100 wenzelm misc tuning and simplification;
Thu, 11 Feb 2010 22:03:37 +0100 wenzelm added ML antiquotation @{syntax_const};
Sun, 07 Feb 2010 18:04:48 +0100 wenzelm simplified interface for ML antiquotations, struct_name is always "Isabelle";
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Wed, 30 Sep 2009 22:20:58 +0200 wenzelm eliminated redundant bindings;
Sat, 28 Mar 2009 17:21:11 +0100 wenzelm renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
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;
Sun, 15 Mar 2009 15:59:43 +0100 wenzelm ML_Syntax.make_binding;
Fri, 13 Mar 2009 21:25:15 +0100 wenzelm eliminated type Args.T;
Sun, 08 Mar 2009 17:26:14 +0100 wenzelm moved basic algebra of long names from structure NameSpace to Long_Name;
Thu, 05 Mar 2009 12:08:00 +0100 wenzelm renamed NameSpace.base to NameSpace.base_name;
Tue, 03 Mar 2009 21:49:05 +0100 wenzelm added @{binding} ML antiquotations;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Fri, 15 Aug 2008 15:50:44 +0200 wenzelm Args.name_source(_position) for proper position information;
Thu, 14 Aug 2008 16:52:54 +0200 wenzelm ML_Context.add_antiq: pass position;
Sat, 09 Aug 2008 22:43:46 +0200 wenzelm unified Args.T with OuterLex.token, renamed some operations;
Sat, 28 Jun 2008 22:52:11 +0200 wenzelm moved theorem values to ml_thms.ML;
Sat, 28 Jun 2008 15:17:28 +0200 wenzelm added macro interface;
Thu, 26 Jun 2008 15:06:25 +0200 wenzelm Args.context;
Wed, 25 Jun 2008 17:38:39 +0200 wenzelm re-use official outer keywords;
Tue, 24 Jun 2008 19:43:16 +0200 wenzelm Common ML antiquotations.
less more (0) tip