| Thu, 24 Jul 2014 20:21:34 +0200 |
store explicitly quotient types with no_code => more precise registration of code equations
|
file | diff | annotate |
| Tue, 25 Feb 2014 15:02:19 +0100 |
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
|
file | diff | annotate |
| Thu, 13 Feb 2014 15:51:54 +0100 |
more precise descripiton
|
file | diff | annotate |
| Thu, 13 Feb 2014 14:32:04 +0100 |
don't catch QOUT_THM_INTERNAL from the recursive call of parametrize_relation_conv
|
file | diff | annotate |
| Wed, 12 Feb 2014 18:32:55 +0100 |
Lifting: support a type variable as a raw type
|
file | diff | annotate |
| Wed, 08 Jan 2014 16:59:57 +0100 |
ensure that schematic type variables are fresh in rty
|
file | diff | annotate |
| Wed, 08 Jan 2014 12:05:42 +0100 |
ensure that the raw type of an abstract type cannot be treated as an abstract type recursively
|
file | diff | annotate |
| Mon, 14 Oct 2013 15:01:41 +0200 |
update documentation of important public ML functions in Lifting
|
file | diff | annotate |
| Mon, 16 Sep 2013 15:30:17 +0200 |
restoring Transfer/Lifting context
|
file | diff | annotate |
| Wed, 28 Aug 2013 14:37:35 +0200 |
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
|
file | diff | annotate |
| Fri, 08 Mar 2013 13:14:23 +0100 |
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 |
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
|
file | diff | annotate |
| Mon, 26 Nov 2012 14:20:51 +0100 |
generate a parameterized correspondence relation
|
file | diff | annotate |
| Mon, 21 May 2012 16:36:48 +0200 |
quot_del attribute, it allows us to deregister quotient types
|
file | diff | annotate |
| Wed, 02 May 2012 19:02:16 +0200 |
resolved maxidx bug
|
file | diff | annotate |
| Wed, 02 May 2012 18:26:10 +0200 |
documentation of the Lifting package on the ML level & tuned
|
file | diff | annotate |
| Thu, 26 Apr 2012 12:03:11 +0200 |
support Quotient map theorems with invariant parameters
|
file | diff | annotate |
| Thu, 26 Apr 2012 12:01:58 +0200 |
use a quot_map theorem attribute instead of the complicated map attribute
|
file | diff | annotate |
| Mon, 23 Apr 2012 17:18:18 +0200 |
move MRSL to a separate file
|
file | diff | annotate |
| Tue, 17 Apr 2012 14:56:38 +0200 |
go back to the explicit compisition of quotient theorems
|
file | diff | annotate |
| Fri, 06 Apr 2012 14:39:27 +0200 |
more robust generation of quotient rules using tactics
|
file | diff | annotate |
| Fri, 06 Apr 2012 10:37:46 +0200 |
add function dest_Quotient
|
file | diff | annotate |
| Thu, 05 Apr 2012 23:22:54 +0200 |
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 |
prove_quot_theorem fixes types
|
file | diff | annotate |
| Tue, 03 Apr 2012 16:26:48 +0200 |
new package Lifting - initial commit
|
file | diff | annotate |