src/HOL/Partial_Function.thy
Thu, 22 Dec 2016 08:43:30 +0100 haftmann proper logical constants
Fri, 29 Jul 2016 09:49:23 +0200 Andreas Lochbihler add lemmas contributed by Peter Gammie
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Sun, 13 Dec 2015 21:56:15 +0100 wenzelm more general types Proof.method / context_tactic;
Mon, 09 Nov 2015 15:48:17 +0100 wenzelm qualifier is mandatory by default;
Wed, 04 Nov 2015 08:13:52 +0100 ballarin Keyword 'rewrites' identifies rewrite morphisms.
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Tue, 14 Apr 2015 13:57:25 +0200 Andreas Lochbihler move lemma from AFP/Coinductive
Sat, 07 Mar 2015 21:32:31 +0100 wenzelm clarified Drule.gen_all: observe context more carefully;
Wed, 11 Feb 2015 14:03:05 +0100 Andreas Lochbihler add lemmas about flat_ord
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Sat, 16 Aug 2014 19:20:11 +0200 wenzelm updated to named_theorems;
Mon, 20 Jan 2014 21:32:41 +0100 blanchet moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
Thu, 05 Dec 2013 09:20:32 +0100 Andreas Lochbihler restrict admissibility to non-empty chains to allow more syntax-directed proof rules
Fri, 27 Sep 2013 12:26:23 +0200 Andreas Lochbihler generalise lemma
Mon, 02 Sep 2013 16:28:11 +0200 Andreas Lochbihler move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
Wed, 24 Jul 2013 17:15:59 +0200 krauss derive specialized version of full fixpoint induction (with admissibility)
Fri, 22 Mar 2013 00:39:16 +0100 krauss added rudimentary induction rule for partial_function (heap)
Tue, 19 Mar 2013 13:19:21 +0100 Andreas Lochbihler add induction rule for partial_function (tailrec)
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Thu, 29 Dec 2011 18:54:07 +0100 huffman remove constant 'ccpo.lub', re-use constant 'Sup' instead
Sat, 29 Oct 2011 12:55:34 +0200 wenzelm tuned;
Tue, 31 May 2011 11:16:34 +0200 krauss generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
Tue, 31 May 2011 11:11:17 +0200 krauss admissibility on option type
Mon, 23 May 2011 21:34:37 +0200 krauss also manage induction rule;
Mon, 23 May 2011 10:58:21 +0200 krauss separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform
Fri, 29 Oct 2010 21:41:14 +0200 krauss added rule let_mono
Fri, 29 Oct 2010 11:04:41 +0200 krauss hide_const various constants, in particular to avoid ugly qualifiers in HOLCF
Sat, 23 Oct 2010 23:41:19 +0200 krauss first version of partial_function package
less more (0) tip