Thu, 19 Apr 2012 08:45:13 +0200 |
generate abs_induct rules for quotient types
|
file | diff | annotate |
Wed, 18 Apr 2012 23:57:44 +0200 |
setup_lifting: no_code switch and supoport for quotient theorems
|
file | diff | annotate |
Wed, 18 Apr 2012 17:04:03 +0200 |
Lifting: generate more thms & note them & tuned
|
file | diff | annotate |
Wed, 18 Apr 2012 12:15:20 +0200 |
lifting_setup generates transfer rule for rep of typedefs
|
file | diff | annotate |
Wed, 18 Apr 2012 10:52:49 +0200 |
use context block to organize typedef lifting theorems
|
file | diff | annotate |
Tue, 17 Apr 2012 19:16:13 +0200 |
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
|
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 17:51:12 +0200 |
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
|
file | diff | annotate |
Wed, 04 Apr 2012 11:50:08 +0200 |
fix typos
|
file | diff | annotate |
Wed, 04 Apr 2012 10:38:04 +0200 |
fix typo in ML structure name
|
file | diff | annotate |
Tue, 03 Apr 2012 16:26:48 +0200 |
new package Lifting - initial commit
|
file | diff | annotate |