src/HOL/Tools/Quotient/quotient_def.ML
Fri, 28 Oct 2011 23:10:44 +0200 wenzelm more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
Fri, 28 Oct 2011 22:17:30 +0200 wenzelm uniform Local_Theory.declaration with explicit params;
Thu, 27 Oct 2011 20:26:38 +0200 wenzelm simplified/standardized signatures;
Tue, 05 Jul 2011 09:54:39 +0200 krauss re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
Thu, 30 Jun 2011 10:15:46 +0200 krauss parse term in auxiliary context augmented with variable;
Wed, 27 Apr 2011 20:58:40 +0200 wenzelm tuned signature -- eliminated odd comment;
Sat, 16 Apr 2011 12:46:18 +0200 wenzelm tuned signature, disentangled dependencies;
Fri, 07 Jan 2011 21:26:49 +0100 wenzelm do not open ML structures;
Fri, 07 Jan 2011 15:35:00 +0100 wenzelm more precise parentheses and indentation;
Sun, 22 Aug 2010 10:45:53 +0800 Christian Urban changed to a more convenient argument order
Thu, 08 Jul 2010 16:19:24 +0200 haftmann tuned titles
Mon, 28 Jun 2010 16:20:39 +0100 Christian Urban separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Mon, 28 Jun 2010 09:48:36 +0200 Cezary Kaliszyk Quotient package reverse lifting
Mon, 28 Jun 2010 07:38:39 +0200 Cezary Kaliszyk Add reverse lifting flag to automated theorem derivation
Mon, 28 Jun 2010 07:32:51 +0200 Cezary Kaliszyk Restrict quotient definitions to constants
Sun, 27 Jun 2010 08:33:01 +0100 Christian Urban mixfix can be given for automatically lifted constants
Thu, 24 Jun 2010 16:27:40 +0100 Christian Urban slight cleaning and simplification of the automatic wrapper for quotient definitions
Thu, 24 Jun 2010 12:33:51 +0100 Christian Urban export of proper information in the ML-interface of the quotient package
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Sun, 16 May 2010 00:02:11 +0200 wenzelm prefer structure Parse_Spec;
Sun, 11 Apr 2010 15:42:05 +0200 wenzelm stay within Local_Defs layer;
Sat, 27 Mar 2010 14:48:46 +0100 Cezary Kaliszyk Automated lifting can be restricted to specific quotient types
Sun, 14 Mar 2010 14:31:24 +0100 wenzelm observe standard header format;
Sun, 07 Mar 2010 11:57:16 +0100 wenzelm modernized structure Local_Defs;
Fri, 19 Feb 2010 13:54:19 +0100 Cezary Kaliszyk Initial version of HOL quotient package.
less more (0) tip