src/HOL/Tools/enriched_type.ML
Thu, 15 Mar 2012 20:07:00 +0100 prefer formally checked @{keyword} parser;
Fri, 09 Mar 2012 21:17:21 +0100 more precise checking for wellformedness of mapper, before and after morphism application
Fri, 09 Mar 2012 20:50:28 +0100 reject mapper terms with type variables not contained in the term's type
Sun, 04 Mar 2012 11:03:10 +0100 tuned
Fri, 28 Oct 2011 22:17:30 +0200 uniform Local_Theory.declaration with explicit params;
Thu, 09 Jun 2011 20:22:22 +0200 tuned signature: Name.invent and Name.invent_names;
Mon, 18 Apr 2011 13:52:23 +0200 standardized aliases of operations on tsig;
Sat, 16 Apr 2011 16:15:37 +0200 modernized structure Proof_Context;
Tue, 11 Jan 2011 14:12:37 +0100 "enriched_type" replaces less specific "type_lifting"