src/HOL/Transfer.thy
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Fri, 28 Oct 2016 19:54:41 +0200 kuncar a more general relator domain rule for the function type
Mon, 03 Oct 2016 14:34:32 +0200 haftmann more lemmas
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";
Tue, 16 Feb 2016 22:28:19 +0100 traytel make predicator a first-class bnf citizen
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
Wed, 11 Feb 2015 15:03:21 +0100 Andreas Lochbihler more transfer rules
Wed, 11 Feb 2015 13:52:12 +0100 Andreas Lochbihler add parametricity rule for Ex1
Wed, 11 Feb 2015 13:51:16 +0100 Andreas Lochbihler add intro and elim rules for right_total
Mon, 05 Jan 2015 06:56:15 +0100 blanchet tuning
Fri, 19 Dec 2014 14:06:13 +0100 desharna Add plugin to generate transfer theorem for primrec and primcorec
Mon, 15 Dec 2014 07:20:48 +0100 blanchet renamed theory file
Fri, 07 Nov 2014 11:28:37 +0100 traytel more complete fp_sugars for sum and prod;
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;
Thu, 25 Sep 2014 16:35:56 +0200 desharna generate 'corec_transfer' for codatatypes
Thu, 25 Sep 2014 16:35:50 +0200 desharna generate 'ctor_rec_transfer' for datatypes
Fri, 19 Sep 2014 10:40:56 +0200 traytel typo
Thu, 04 Sep 2014 11:20:59 +0200 blanchet tweaked setup for datatype realizer
Mon, 01 Sep 2014 16:34:40 +0200 blanchet renamed BNF theories
Mon, 21 Jul 2014 17:51:29 +0200 Andreas Lochbihler add parametricity lemmas
Fri, 27 Jun 2014 10:11:44 +0200 blanchet merged two small theory files
Mon, 16 Jun 2014 19:18:10 +0200 blanchet fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
Wed, 23 Apr 2014 17:57:56 +0200 kuncar predicator simplification rules: support also partially specialized types e.g. 'a * nat
Wed, 23 Apr 2014 10:23:27 +0200 blanchet qualify name
Fri, 11 Apr 2014 23:22:00 +0200 kuncar bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced
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:14 +0200 kuncar left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
Thu, 13 Mar 2014 13:18:13 +0100 blanchet killed a few 'metis' calls
Thu, 06 Mar 2014 15:40:33 +0100 blanchet renamed 'fun_rel' to 'rel_fun'
Fri, 28 Feb 2014 17:54:52 +0100 traytel load Metis a little later
Wed, 26 Feb 2014 16:48:15 +0100 kuncar transfer domain rule for special case of functions - was missing
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed 'nat_{case,rec}' to '{case,rec}_nat'
Mon, 20 Jan 2014 20:42:43 +0100 blanchet rationalized lemmas
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
Tue, 13 Aug 2013 15:59:22 +0200 kuncar introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
Mon, 10 Jun 2013 06:08:12 -0700 huffman implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
Sat, 08 Jun 2013 19:40:19 -0700 huffman implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
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
Mon, 13 May 2013 12:13:24 +0200 kuncar try to detect assumptions of transfer rules that are in a shape of a transfer rule
Sat, 16 Mar 2013 20:51:23 +0100 kuncar fixing transfer tactic - unfold fully identity relation by using relator_eq
Thu, 14 Feb 2013 12:24:42 +0100 haftmann abandoned theory Plain
Wed, 24 Oct 2012 18:43:25 +0200 huffman transfer package: more flexible handling of equality relations using is_equality predicate
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
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
Tue, 15 May 2012 11:50:34 +0200 huffman add transfer rules for nat_rec and funpow
Fri, 27 Apr 2012 14:07:31 +0200 huffman implement transfer tactic with more scalable forward proof methods
Sun, 22 Apr 2012 21:32:35 +0200 huffman tuned precedence order of transfer rules
Sun, 22 Apr 2012 11:05:04 +0200 huffman new example theory for quotient/transfer
Sat, 21 Apr 2012 20:52:33 +0200 huffman enable variant of transfer method that proves an implication instead of an equivalence
Fri, 20 Apr 2012 22:05:07 +0200 huffman add transfer rule for nat_case
Fri, 20 Apr 2012 22:54:13 +0200 huffman uniform naming scheme for transfer rules
Fri, 20 Apr 2012 22:49:40 +0200 huffman rename 'correspondence' method to 'transfer_prover'
Fri, 20 Apr 2012 15:49:45 +0200 huffman add secondary transfer rule for universal quantifiers on non-bi-total relations
less more (0) -60 tip