src/HOL/Tools/typedef.ML
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
Sun, 25 Apr 2010 15:52:03 +0200 wenzelm modernized naming conventions of main Isar proof elements;
Thu, 15 Apr 2010 18:09:22 +0200 wenzelm replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
Sun, 11 Apr 2010 15:22:15 +0200 wenzelm expose foundational typedef axiom name;
Sun, 11 Apr 2010 14:30:34 +0200 wenzelm Thm.add_axiom/add_def: return internal name of foundational axiom;
Sat, 27 Mar 2010 21:38:38 +0100 wenzelm Typedef.info: separate global and local part, only the latter is transformed by morphisms;
Fri, 19 Mar 2010 00:43:49 +0100 wenzelm allow sort constraints in HOL/typedef and related HOLCF variants;
Thu, 18 Mar 2010 23:00:18 +0100 wenzelm eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints;
Sat, 13 Mar 2010 20:34:22 +0100 wenzelm Local_Theory.define handles hidden polymorphism;
Sat, 13 Mar 2010 14:42:16 +0100 wenzelm localized typedef;
Tue, 09 Mar 2010 23:32:49 +0100 wenzelm Typedecl.typedecl_global;
Sun, 07 Mar 2010 12:47:02 +0100 wenzelm separate structure Typedecl;
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Wed, 03 Mar 2010 00:32:14 +0100 wenzelm adapted to authentic syntax -- actual types are verbatim;
Wed, 24 Feb 2010 20:37:01 +0100 wenzelm allow general mixfix syntax for type constructors;
Fri, 19 Feb 2010 20:41:34 +0100 wenzelm Thm.def_binding;
Thu, 18 Feb 2010 23:08:31 +0100 wenzelm typedef: slightly more precise treatment of binding;
Mon, 15 Feb 2010 20:30:56 +0100 wenzelm Typedef.the_info;
Mon, 15 Feb 2010 17:17:51 +0100 wenzelm discontinued unnamed infix syntax;
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Sun, 08 Nov 2009 18:43:42 +0100 wenzelm adapted Theory_Data;
Mon, 02 Nov 2009 20:38:46 +0100 wenzelm modernized structure Primitive_Defs;
Sun, 01 Nov 2009 15:24:45 +0100 wenzelm modernized structure Rule_Cases;
Thu, 29 Oct 2009 16:15:33 +0100 wenzelm modernized functor/structures Interpretation;
Sat, 17 Oct 2009 16:58:03 +0200 wenzelm operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
Sat, 17 Oct 2009 15:57:51 +0200 wenzelm indicate CRITICAL nature of various setmp combinators;
Sun, 21 Jun 2009 08:38:57 +0200 haftmann tuned interface
Fri, 19 Jun 2009 17:23:21 +0200 haftmann discontinued ancient tradition to suffix certain ML module names with "_package"
less more (0) tip