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