src/HOL/Tools/Lifting/lifting_def.ML
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