| Tue, 23 Aug 2011 03:34:17 +0900 |
Cezary Kaliszyk |
Quotient Package: some infrastructure for lifting inside sets
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
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
|
| Thu, 28 Oct 2010 22:11:06 +0200 |
wenzelm |
handle Type.TYPE_MATCH, not arbitrary exceptions via MATCH_TYPE variable;
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 20:04:49 +0800 |
Christian Urban |
tuned code
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 22:38:45 +0800 |
Christian Urban |
use matching of types than just equality - this is needed in nominal to cope with type variables
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 10:45:53 +0800 |
Christian Urban |
changed to a more convenient argument order
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 16:08:59 +0200 |
haftmann |
tuned quotes
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 16:54:42 +0200 |
haftmann |
qualified constants Set.member and Set.Collect
|
file |
diff |
annotate
|
| Tue, 29 Jun 2010 09:37:23 +0100 |
Christian Urban |
tuned
|
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 15:03:07 +0200 |
haftmann |
merged constants "split" and "prod_case"
|
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
|
| Sat, 26 Jun 2010 08:23:40 +0100 |
Christian Urban |
streamlined the generation of quotient theorems out of raw theorems
|
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
|
| Wed, 26 May 2010 16:05:25 +0200 |
haftmann |
normalized references to constant "split"
|
file |
diff |
annotate
|
| Wed, 05 May 2010 18:25:34 +0200 |
haftmann |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
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
|
| Fri, 19 Mar 2010 06:14:37 +0100 |
Cezary Kaliszyk |
Check that argument is not a 'Bound' before calling fastype_of.
|
file |
diff |
annotate
|
| Sun, 14 Mar 2010 14:31:24 +0100 |
wenzelm |
observe standard header format;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 20:57:08 +0100 |
wenzelm |
clarified @{const_name} vs. @{const_abbrev};
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 13:54:19 +0100 |
Cezary Kaliszyk |
Initial version of HOL quotient package.
|
file |
diff |
annotate
|