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