src/HOL/Tools/TFL/casesplit.ML
Tue, 02 Jun 2015 13:55:43 +0200 wenzelm clarified context;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Sat, 08 Nov 2014 21:31:51 +0100 wenzelm optional proof context for unify operations, for the sake of proper local options;
Wed, 17 Sep 2014 08:23:53 +0200 blanchet support (finite values of) codatatypes in Quickcheck
Mon, 01 Sep 2014 19:57:48 +0200 blanchet ported TFL to mixture of old and new datatypes
Mon, 01 Sep 2014 16:17:46 +0200 blanchet renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
Mon, 01 Sep 2014 16:17:46 +0200 blanchet tuned structure inclusion
Sat, 01 Feb 2014 18:42:46 +0100 wenzelm proper context for printing;
Thu, 30 May 2013 17:02:09 +0200 wenzelm prefer existing beta_eta_conversion;
Wed, 12 Sep 2012 23:18:26 +0200 wenzelm observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
Wed, 15 Feb 2012 20:28:19 +0100 wenzelm removed dead code;
Wed, 30 Nov 2011 23:30:08 +0100 wenzelm discontinued obsolete datatype "alt_names";
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy;
Sat, 16 Apr 2011 20:22:50 +0200 wenzelm more direct Logic.dest_implies (with exception TERM instead of Subscript);
Sat, 16 Apr 2011 18:11:20 +0200 wenzelm eliminated old List.nth;
less more (0) -15 tip