src/HOL/Tools/Quotient/quotient_def.ML
Mon, 11 Apr 2016 15:07:15 +0200 wenzelm tuned message;
Wed, 30 Mar 2016 23:46:44 +0200 wenzelm proper object-logic constraint (amending dd2914250ca7);
Sat, 18 Jul 2015 20:47:08 +0200 wenzelm prefer tactics with explicit context;
Mon, 06 Jul 2015 19:33:30 +0200 wenzelm tuned;
Sun, 07 Jun 2015 20:03:40 +0200 wenzelm tuned signature;
Mon, 06 Apr 2015 17:06:48 +0200 wenzelm @{command_spec} is superseded by @{command_keyword};
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Tue, 03 Mar 2015 19:08:04 +0100 traytel eliminated some clones of Proof_Context.cterm_of
Fri, 19 Dec 2014 21:59:18 +0100 wenzelm just one data slot per program unit;
Sat, 16 Aug 2014 20:14:45 +0200 wenzelm updated to named_theorems;
Thu, 10 Apr 2014 17:48:18 +0200 kuncar setup for Transfer and Lifting from BNF; tuned thm names
Thu, 10 Apr 2014 17:48:15 +0200 kuncar more appropriate name (Lifting.invariant -> eq_onp)
Thu, 06 Mar 2014 15:40:33 +0100 blanchet renamed 'fun_rel' to 'rel_fun'
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Tue, 15 Jan 2013 17:28:46 +0100 wenzelm avoid handling arbitrary exceptions, notably physical interrupts that would make the program erratic;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Wed, 16 May 2012 19:20:19 +0200 kuncar remove the generation of a code certificate from the Quotient package (mainly from quotient_def), because it's in lift_definition now
Mon, 23 Apr 2012 17:18:18 +0200 kuncar move MRSL to a separate file
Tue, 17 Apr 2012 14:56:38 +0200 kuncar go back to the explicit compisition of quotient theorems
Tue, 10 Apr 2012 16:10:50 +0100 Christian Urban moved lift_raw_const wrapper out of the Quotient-package into Nominal2
Thu, 05 Apr 2012 22:00:27 +0200 kuncar make Quotient_Def.lift_raw_const working again
Tue, 03 Apr 2012 16:26:48 +0200 kuncar new package Lifting - initial commit
Thu, 29 Mar 2012 21:13:48 +0200 kuncar use qualified names for rsp and rep_eq theorems in quotient_def
Wed, 28 Mar 2012 10:44:04 +0200 bulwahn some tuning while reviewing the current state of the quotient_def package
Tue, 27 Mar 2012 14:46:34 +0200 kuncar note a code eqn in quotient_def
Fri, 23 Mar 2012 14:25:31 +0100 kuncar generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
Fri, 23 Mar 2012 14:03:58 +0100 kuncar respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations;
Thu, 15 Mar 2012 20:07:00 +0100 wenzelm prefer formally checked @{keyword} parser;
Tue, 13 Mar 2012 20:04:24 +0100 wenzelm more explicit indication of def names;
Tue, 20 Dec 2011 17:40:21 +0100 bulwahn removing some debug output in quotient_definition
Tue, 13 Dec 2011 14:04:20 +0100 kuncar support phantom types as quotient types
Fri, 09 Dec 2011 14:14:37 +0100 kuncar make ctxt the first parameter
Sun, 20 Nov 2011 17:04:59 +0100 wenzelm more uniform signature;
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