src/HOL/Tools/Lifting/lifting_def.ML
Mon, 26 Aug 2013 16:13:20 +0200 wenzelm prefer Binding.name_of over Binding.print -- the latter leads to funny quotes and markup within the constructed term;
Mon, 26 Aug 2013 15:45:51 +0200 wenzelm proper context;
Wed, 15 May 2013 12:10:39 +0200 kuncar stronger reflexivity prover
Mon, 13 May 2013 15:22:19 +0200 kuncar typo
Fri, 10 May 2013 19:41:23 +0200 kuncar don't apply an unnecessary morphism
Fri, 08 Mar 2013 13:14:23 +0100 kuncar lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
Thu, 28 Feb 2013 16:54:52 +0100 wenzelm just one HOLogic.Trueprop_conv, with regular exception CTERM;
Wed, 24 Oct 2012 18:43:25 +0200 huffman transfer package: more flexible handling of equality relations using is_equality predicate
Wed, 17 Oct 2012 00:16:31 +0200 kuncar don't be so aggressive when expanding a transfer rule relation; rewrite only the relational part of the rule
Thu, 27 Sep 2012 20:30:32 +0200 kuncar mk_readable_rsp_thm_eq is more robust now
Thu, 27 Sep 2012 20:30:30 +0200 kuncar new get function for non-symmetric relator_eq & tuned
Tue, 29 May 2012 19:13:02 +0200 kuncar don't be so aggressive during unfolding id and o
Thu, 24 May 2012 14:20:23 +0200 kuncar prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
Mon, 21 May 2012 16:36:48 +0200 kuncar quot_del attribute, it allows us to deregister quotient types
Wed, 16 May 2012 19:17:20 +0200 kuncar 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
Wed, 02 May 2012 18:26:10 +0200 kuncar documentation of the Lifting package on the ML level & tuned
Mon, 23 Apr 2012 18:42:03 +0200 kuncar added useful Trueprop_conv
Mon, 23 Apr 2012 17:18:18 +0200 kuncar move MRSL to a separate file
Sun, 22 Apr 2012 16:53:24 +0200 huffman fix bug caused by misunderstanding of operator precedences (cf. cb44d09d9d22)
Fri, 20 Apr 2012 18:29:21 +0200 kuncar hide the invariant constant for relators: invariant_commute infrastracture
Thu, 19 Apr 2012 17:31:34 +0200 kuncar use tnames for bound variables in rsp thms
Wed, 18 Apr 2012 23:57:44 +0200 kuncar setup_lifting: no_code switch and supoport for quotient theorems
Wed, 18 Apr 2012 17:04:03 +0200 kuncar Lifting: generate more thms & note them & tuned
Tue, 17 Apr 2012 14:56:38 +0200 kuncar go back to the explicit compisition of quotient theorems
Tue, 17 Apr 2012 11:03:08 +0200 huffman add theory data for relator identity rules;
Fri, 06 Apr 2012 14:39:27 +0200 huffman more robust generation of quotient rules using tactics
Fri, 06 Apr 2012 09:35:47 +0200 huffman correct plumbing of proof contexts, so that force_rty_type won't generalize more type variables than it should
Thu, 05 Apr 2012 23:22:54 +0200 kuncar detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
Thu, 05 Apr 2012 12:18:06 +0200 huffman lift_definition declares transfer_rule attribute
Wed, 04 Apr 2012 17:51:12 +0200 kuncar support non-open typedefs; define cr_rel in terms of a rep function for typedefs
Wed, 04 Apr 2012 13:42:01 +0200 huffman lift_definition command generates transfer rule
Tue, 03 Apr 2012 16:26:48 +0200 kuncar new package Lifting - initial commit
less more (0) tip