Fri, 08 Mar 2013 13:21:55 +0100 | kuncar | setup_lifting doesn't support a type variable as a raw type | changeset | files |
Fri, 08 Mar 2013 13:21:52 +0100 | kuncar | add [relator_mono] and [relator_distr] rules | changeset | files |
Fri, 08 Mar 2013 13:21:45 +0100 | kuncar | simplify Lift_FSet because we have parametricity in Lifting now | changeset | files |
Fri, 08 Mar 2013 13:21:06 +0100 | kuncar | patch Isabelle ditribution to conform to changes regarding the parametricity | changeset | files |
Fri, 08 Mar 2013 13:14:23 +0100 | kuncar | lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided | changeset | files |
Fri, 08 Mar 2013 11:28:20 +0100 | nipkow | merged | changeset | files |
Fri, 08 Mar 2013 11:28:04 +0100 | nipkow | simplified basic termination proof | changeset | files |