| Wed, 18 Apr 2012 23:57:44 +0200 |
kuncar |
setup_lifting: no_code switch and supoport for quotient theorems
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 17:04:03 +0200 |
kuncar |
Lifting: generate more thms & note them & tuned
|
file |
diff |
annotate
|
| Tue, 17 Apr 2012 14:56:38 +0200 |
kuncar |
go back to the explicit compisition of quotient theorems
|
file |
diff |
annotate
|
| Tue, 17 Apr 2012 11:03:08 +0200 |
huffman |
add theory data for relator identity rules;
|
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 09:35:47 +0200 |
huffman |
correct plumbing of proof contexts, so that force_rty_type won't generalize more type variables than it should
|
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
|
| Thu, 05 Apr 2012 12:18:06 +0200 |
huffman |
lift_definition declares transfer_rule attribute
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 17:51:12 +0200 |
kuncar |
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 13:42:01 +0200 |
huffman |
lift_definition command generates transfer rule
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 16:26:48 +0200 |
kuncar |
new package Lifting - initial commit
|
file |
diff |
annotate
|