src/HOL/Lifting_Set.thy
Wed, 23 Oct 2019 16:09:23 +0000 haftmann tuned syntax
Sat, 10 Nov 2018 07:57:19 +0000 haftmann clarified status of legacy input abbreviations
Wed, 27 Jun 2018 10:18:03 +0200 immler added lemmas and transfer rules
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Mon, 17 Oct 2016 17:33:07 +0200 nipkow setprod -> prod
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Wed, 22 Jun 2016 10:09:20 +0200 wenzelm bundle lifting_syntax;
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Wed, 17 Feb 2016 21:51:56 +0100 haftmann prefer abbreviations for compound operators INFIMUM and SUPREMUM
Mon, 28 Dec 2015 17:43:30 +0100 wenzelm prefer symbols for "Union", "Inter";
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Mon, 06 Jul 2015 21:20:28 +0200 wenzelm tuned proofs;
Fri, 05 Dec 2014 14:14:36 +0100 kuncar Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
Tue, 14 Apr 2015 11:32:01 +0200 Andreas Lochbihler add lemmas
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Mon, 01 Sep 2014 13:23:39 +0200 desharna generate 'rel_transfer' for BNFs
Mon, 21 Jul 2014 17:51:29 +0200 Andreas Lochbihler add parametricity lemmas
Fri, 30 May 2014 14:55:10 +0200 hoelzl introduce more powerful reindexing rules for big operators
Thu, 10 Apr 2014 17:48:18 +0200 kuncar setup for Transfer and Lifting from BNF; tuned thm names
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)
Wed, 09 Apr 2014 10:04:31 +0200 haftmann parametricity transfer rule for INFIMUM, SUPREMUM
Wed, 19 Mar 2014 18:47:22 +0100 haftmann elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
Tue, 18 Mar 2014 22:11:46 +0100 haftmann consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
Sun, 16 Mar 2014 18:09:04 +0100 haftmann normalising simp rules for compound operators
Thu, 06 Mar 2014 15:40:33 +0100 blanchet renamed 'fun_rel' to 'rel_fun'
Thu, 06 Mar 2014 14:57:14 +0100 blanchet renamed 'set_rel' to 'rel_set'
Tue, 18 Feb 2014 23:03:49 +0100 kuncar delete or move now not necessary reflexivity rules due to 1726f46d2aa8
Tue, 05 Nov 2013 09:44:57 +0100 hoelzl generalize SUP and INF to the syntactic type classes Sup and Inf
Fri, 27 Sep 2013 14:43:26 +0200 kuncar new parametricity rules and useful lemmas
Fri, 27 Sep 2013 09:15:40 +0200 Andreas Lochbihler tuned proofs
Thu, 26 Sep 2013 15:50:33 +0200 Andreas Lochbihler add lemmas
Tue, 13 Aug 2013 15:59:22 +0200 kuncar move Lifting/Transfer relevant parts of Library/Quotient_* to Main
less more (0) tip