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
|