src/HOL/Partial_Function.thy
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;
less more (0) -15 tip