| Sun, 22 Aug 2010 10:45:53 +0800 |
Christian Urban |
changed to a more convenient argument order
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 13:30:24 +0800 |
Christian Urban |
deleted duplicate lemma
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Tue, 29 Jun 2010 01:38:29 +0100 |
Christian Urban |
separated the lifting and descending procedures in the quotient package
|
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
|
| Sat, 26 Jun 2010 08:23:40 +0100 |
Christian Urban |
streamlined the generation of quotient theorems out of raw theorems
|
file |
diff |
annotate
|
| Wed, 23 Jun 2010 08:44:44 +0200 |
Cezary Kaliszyk |
Quotient package now uses Partial Equivalence instead place of equivalence
|
file |
diff |
annotate
|
| Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 17:59:06 +0200 |
wenzelm |
incorporated further conversions and conversionals, after some minor tuning;
|
file |
diff |
annotate
|
| Wed, 12 May 2010 11:30:18 +0200 |
Cezary Kaliszyk |
Remove RANGE_WARN
|
file |
diff |
annotate
|
| Mon, 03 May 2010 20:13:36 +0200 |
wenzelm |
renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
|
file |
diff |
annotate
|
| Tue, 20 Apr 2010 14:55:53 +0200 |
Cezary Kaliszyk |
eta-normalize the goal since the original theorem is atomized
|
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:36:56 +0100 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Sun, 14 Mar 2010 14:31:24 +0100 |
wenzelm |
observe standard header format;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 13:54:19 +0100 |
Cezary Kaliszyk |
Initial version of HOL quotient package.
|
file |
diff |
annotate
|