| Thu, 24 Jul 2014 20:21:34 +0200 |
store explicitly quotient types with no_code => more precise registration of code equations
|
file | diff | annotate |
| Thu, 10 Apr 2014 17:48:15 +0200 |
more appropriate name (Lifting.invariant -> eq_onp)
|
file | diff | annotate |
| Thu, 10 Apr 2014 17:48:14 +0200 |
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
|
file | diff | annotate |
| Sat, 22 Mar 2014 21:40:19 +0100 |
more antiquotations;
|
file | diff | annotate |
| Mon, 10 Mar 2014 21:40:39 +0100 |
proper Args.syntax for slightly odd bundle trickery;
|
file | diff | annotate |
| Mon, 10 Mar 2014 16:30:07 +0100 |
clarified Args.src: more abstract type, position refers to name only;
|
file | diff | annotate |
| Mon, 10 Mar 2014 15:04:01 +0100 |
tuned signature -- prefer Name_Space.get with its builtin error;
|
file | diff | annotate |
| Tue, 18 Feb 2014 23:03:47 +0100 |
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
|
file | diff | annotate |
| Sat, 15 Feb 2014 00:11:17 +0100 |
abstract type must be a type constructor; check it
|
file | diff | annotate |
| Mon, 14 Oct 2013 15:01:41 +0200 |
update documentation of important public ML functions in Lifting
|
file | diff | annotate |
| Fri, 11 Oct 2013 18:36:51 +0200 |
don't allow parametricity theorem for typedefs in setup_lifting. The theorem is not used.
|
file | diff | annotate |
| Fri, 20 Sep 2013 17:08:08 +0200 |
make SML/NJ happy
|
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 |
| Wed, 07 Aug 2013 15:40:29 +0200 |
expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
|
file | diff | annotate |
| Wed, 15 May 2013 12:10:39 +0200 |
stronger reflexivity prover
|
file | diff | annotate |
| Mon, 13 May 2013 13:59:04 +0200 |
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
|
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 17:13:44 +0100 |
merged
|
file | diff | annotate |
| Mon, 26 Nov 2012 14:20:51 +0100 |
generate a parameterized correspondence relation
|
file | diff | annotate |
| Mon, 26 Nov 2012 14:43:28 +0100 |
tuned command descriptions;
|
file | diff | annotate |
| Fri, 23 Nov 2012 15:53:24 +0100 |
simplified code
|
file | diff | annotate |
| Fri, 23 Nov 2012 15:53:19 +0100 |
generate correct correspondence relation name
|
file | diff | annotate |
| Thu, 24 May 2012 14:20:23 +0200 |
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
|
file | diff | annotate |
| Mon, 21 May 2012 16:36:48 +0200 |
quot_del attribute, it allows us to deregister quotient types
|
file | diff | annotate |
| Fri, 18 May 2012 17:36:20 +0200 |
note Quotient theorem for typedefs in setup_lifting
|
file | diff | annotate |
| Wed, 16 May 2012 19:17:20 +0200 |
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
|
file | diff | annotate |
| Wed, 16 May 2012 19:15:45 +0200 |
infrastructure that makes possible to prove that a relation is reflexive
|
file | diff | annotate |
| Fri, 04 May 2012 17:12:37 +0200 |
lifting package produces abs_eq_iff rules for total quotients
|
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 14:11:13 +0200 |
tuned; don't generate abs code if quotient_type is used
|
file | diff | annotate |
| Mon, 23 Apr 2012 17:18:18 +0200 |
move MRSL to a separate file
|
file | diff | annotate |
| Fri, 20 Apr 2012 10:37:00 +0200 |
setup_lifting preprocesses forall_transfer rule by unfolding mem_Collect_eq
|
file | diff | annotate |
| Thu, 19 Apr 2012 18:24:40 +0200 |
rename no_code to no_abs_code - more appropriate name
|
file | diff | annotate |
| Thu, 19 Apr 2012 12:28:10 +0200 |
create thm names correctly
|
file | diff | annotate |
| 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 |