src/HOL/Lifting.thy
Tue, 10 Dec 2019 01:06:39 +0100 traytel extension of lift_bnf to support quotient types
Thu, 14 Mar 2019 16:55:06 +0100 wenzelm more specific keyword kinds;
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Wed, 20 Dec 2017 14:53:34 +0100 nipkow tuned op's
Wed, 22 Jun 2016 10:09:20 +0200 wenzelm bundle lifting_syntax;
Fri, 13 May 2016 20:24:10 +0200 wenzelm eliminated use of empty "assms";
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Wed, 11 Nov 2015 09:48:24 +0100 Andreas Lochbihler add various lemmas
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
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
Mon, 16 Mar 2015 23:05:56 +0100 traytel BNF relators preserve reflexivity
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Wed, 29 Oct 2014 15:02:29 +0100 wenzelm modernized setup;
Fri, 05 Sep 2014 00:41:01 +0200 blanchet named interpretations
Wed, 03 Sep 2014 22:49:05 +0200 blanchet introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
Sat, 16 Aug 2014 20:27:51 +0200 wenzelm updated to named_theorems;
Fri, 27 Jun 2014 10:11:44 +0200 blanchet merged two small theory files
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 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, 10 Apr 2014 17:48:13 +0200 kuncar tuned
Thu, 06 Mar 2014 15:40:33 +0100 blanchet renamed 'fun_rel' to 'rel_fun'
Tue, 25 Feb 2014 19:07:40 +0100 kuncar new rule for making rsp theorem more readable
Tue, 25 Feb 2014 15:02:19 +0100 kuncar rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
Thu, 20 Feb 2014 16:56:33 +0100 kuncar refactoring; generate rep_eq always, not only when it would be accepted by the code generator
Thu, 20 Feb 2014 15:14:37 +0100 noschinl less flex-flex pairs
Tue, 18 Feb 2014 23:03:47 +0100 kuncar implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
Mon, 20 Jan 2014 20:21:12 +0100 blanchet move BNF_LFP up the dependency chain
Fri, 27 Sep 2013 14:43:26 +0200 kuncar new parametricity rules and useful lemmas
Fri, 27 Sep 2013 09:07:45 +0200 Andreas Lochbihler add lemmas
Thu, 26 Sep 2013 15:50:33 +0200 Andreas Lochbihler add lemmas
Mon, 16 Sep 2013 15:30:17 +0200 kuncar restoring Transfer/Lifting context
Wed, 28 Aug 2013 14:37:35 +0200 kuncar use only one data slot; rename print_quotmaps to print_quot_maps; tuned
Fri, 23 Aug 2013 00:12:20 +0200 kuncar remove OP
Tue, 13 Aug 2013 15:59:22 +0200 kuncar introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
Wed, 05 Jun 2013 15:21:52 +0200 kuncar more reflexivity rules (for OO)
Thu, 16 May 2013 15:21:12 +0200 kuncar reflexivity rules for the function type and equality
Wed, 15 May 2013 12:10:39 +0200 kuncar stronger reflexivity prover
Mon, 13 May 2013 13:59:04 +0200 kuncar better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
Fri, 08 Mar 2013 13:14:23 +0100 kuncar lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
Thu, 14 Feb 2013 12:24:42 +0100 haftmann abandoned theory Plain
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Thu, 24 May 2012 14:20:23 +0200 kuncar prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
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, 16 May 2012 19:15:45 +0200 kuncar infrastructure that makes possible to prove that a relation is reflexive
Fri, 04 May 2012 17:12:37 +0200 huffman lifting package produces abs_eq_iff rules for total quotients
Thu, 26 Apr 2012 12:01:58 +0200 kuncar use a quot_map theorem attribute instead of the complicated map attribute
Mon, 23 Apr 2012 17:18:18 +0200 kuncar move MRSL to a separate file
Sat, 21 Apr 2012 13:12:27 +0200 huffman move alternative definition lemmas into Lifting.thy;
Sat, 21 Apr 2012 13:06:22 +0200 huffman tuned proofs
Thu, 19 Apr 2012 08:45:13 +0200 huffman generate abs_induct rules for quotient types
Wed, 18 Apr 2012 17:04:03 +0200 kuncar Lifting: generate more thms & note them & tuned
Wed, 18 Apr 2012 15:48:32 +0200 huffman move constant 'Respects' into Lifting.thy;
Wed, 18 Apr 2012 15:09:07 +0200 huffman add lemma Quotient_abs_induct
Wed, 18 Apr 2012 14:59:04 +0200 huffman more usage of context blocks
Wed, 18 Apr 2012 14:34:25 +0200 huffman use context block
Wed, 18 Apr 2012 12:15:20 +0200 huffman lifting_setup generates transfer rule for rep of typedefs
Wed, 18 Apr 2012 10:52:49 +0200 huffman use context block to organize typedef lifting theorems
Tue, 17 Apr 2012 19:16:13 +0200 kuncar tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
less more (0) -60 tip