src/HOL/Lifting_Sum.thy
Thu, 10 Apr 2014 17:48:32 +0200 kuncar simplify and fix theories thanks to 356a5efdb278
Thu, 10 Apr 2014 17:48:15 +0200 kuncar abstract Domainp in relator_domain rules => more natural statement of the rule
Thu, 10 Apr 2014 17:48:15 +0200 kuncar more appropriate name (Lifting.invariant -> eq_onp)
Thu, 10 Apr 2014 17:48:14 +0200 kuncar left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
Thu, 06 Mar 2014 15:40:33 +0100 blanchet renamed 'fun_rel' to 'rel_fun'
Thu, 06 Mar 2014 15:25:21 +0100 blanchet renamed 'sum_rel' to 'rel_sum'
Thu, 06 Mar 2014 13:36:15 +0100 blanchet renamed 'map_sum' to 'sum_map'
Tue, 18 Feb 2014 23:03:49 +0100 kuncar delete or move now not necessary reflexivity rules due to 1726f46d2aa8
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...'
Mon, 20 Jan 2014 20:42:43 +0100 blanchet rationalized lemmas
Mon, 20 Jan 2014 20:21:12 +0100 blanchet move BNF_LFP up the dependency chain
Tue, 13 Aug 2013 18:22:55 +0200 traytel got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
Tue, 13 Aug 2013 15:59:22 +0200 kuncar move Lifting/Transfer relevant parts of Library/Quotient_* to Main
less more (0) tip