Fri, 08 Mar 2013 13:14:23 +0100 | kuncar | lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided | file | diff | annotate |
Thu, 28 Feb 2013 16:54:52 +0100 | wenzelm | just one HOLogic.Trueprop_conv, with regular exception CTERM; | file | diff | annotate |
Mon, 26 Nov 2012 14:20:36 +0100 | kuncar | quot_thm_crel | file | diff | annotate |
Mon, 26 Nov 2012 14:15:48 +0100 | kuncar | add option_fold | file | diff | annotate |
Mon, 21 May 2012 16:36:48 +0200 | kuncar | quot_del attribute, it allows us to deregister quotient types | file | diff | annotate |
Thu, 26 Apr 2012 12:01:58 +0200 | kuncar | use a quot_map theorem attribute instead of the complicated map attribute | file | diff | annotate |
Mon, 23 Apr 2012 18:42:03 +0200 | kuncar | added useful Trueprop_conv | file | diff | annotate |
Mon, 23 Apr 2012 17:18:18 +0200 | kuncar | move MRSL to a separate file | file | diff | annotate |