| Fri, 08 Mar 2013 13:14:23 +0100 |
kuncar |
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
|
file |
diff |
annotate
|
| Thu, 29 Nov 2012 17:54:20 +0100 |
kuncar |
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 14:20:51 +0100 |
kuncar |
generate a parameterized correspondence relation
|
file |
diff |
annotate
|
| Mon, 21 May 2012 16:36:48 +0200 |
kuncar |
quot_del attribute, it allows us to deregister quotient types
|
file |
diff |
annotate
|
| Wed, 02 May 2012 19:02:16 +0200 |
kuncar |
resolved maxidx bug
|
file |
diff |
annotate
|
| Wed, 02 May 2012 18:26:10 +0200 |
kuncar |
documentation of the Lifting package on the ML level & tuned
|
file |
diff |
annotate
|
| Thu, 26 Apr 2012 12:03:11 +0200 |
kuncar |
support Quotient map theorems with invariant parameters
|
file |
diff |
annotate
|
| Thu, 26 Apr 2012 12:01:58 +0200 |
kuncar |
use a quot_map theorem attribute instead of the complicated map attribute
|
file |
diff |
annotate
|
| Mon, 23 Apr 2012 17:18:18 +0200 |
kuncar |
move MRSL to a separate file
|
file |
diff |
annotate
|
| Tue, 17 Apr 2012 14:56:38 +0200 |
kuncar |
go back to the explicit compisition of quotient theorems
|
file |
diff |
annotate
|
| Fri, 06 Apr 2012 14:39:27 +0200 |
huffman |
more robust generation of quotient rules using tactics
|
file |
diff |
annotate
|
| Fri, 06 Apr 2012 10:37:46 +0200 |
huffman |
add function dest_Quotient
|
file |
diff |
annotate
|
| Thu, 05 Apr 2012 23:22:54 +0200 |
kuncar |
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 13:41:38 +0200 |
huffman |
prove_quot_theorem fixes types
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 16:26:48 +0200 |
kuncar |
new package Lifting - initial commit
|
file |
diff |
annotate
|