src/HOL/Tools/Function/function_core.ML
Wed, 29 May 2013 18:25:11 +0200 wenzelm tuned signature -- more explicit flags for low-level Thm.bicompose;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Wed, 05 Sep 2012 19:51:00 +0200 wenzelm discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
Sat, 14 Jan 2012 19:06:05 +0100 wenzelm renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
Fri, 13 May 2011 22:55:00 +0200 wenzelm proper Proof.context for classical tactics;
Wed, 27 Apr 2011 10:49:39 +0200 wenzelm eliminated obsolete Function_Lib.frees_in_term;
Sat, 16 Apr 2011 16:29:13 +0200 wenzelm observe firm naming convention ctxt: Proof.context;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Fri, 25 Feb 2011 16:59:48 +0100 krauss removed support for tail-recursion from function package (now implemented by partial_function)
Wed, 29 Dec 2010 21:52:41 +0100 krauss function (default) is legacy feature
Sun, 12 Dec 2010 21:41:01 +0100 krauss tuned headers
Sun, 12 Sep 2010 19:04:02 +0200 wenzelm eliminated aliases of Type.constraint;
Tue, 31 Aug 2010 10:00:06 +0200 krauss more permissive: simplification solves the goal when rhs = undefined
Thu, 19 Aug 2010 16:08:59 +0200 haftmann tuned quotes
Thu, 19 Aug 2010 11:02:14 +0200 haftmann use antiquotations for remaining unqualified constants in HOL
Thu, 27 May 2010 17:41:27 +0200 wenzelm renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
Sat, 15 May 2010 21:50:05 +0200 wenzelm less pervasive names from structure Thm;
Sat, 15 May 2010 17:59:06 +0200 wenzelm incorporated further conversions and conversionals, after some minor tuning;
Wed, 21 Apr 2010 15:45:33 +0200 krauss tolerate eta-variants in f_graph.cases (from inductive package); added test case;
Sat, 02 Jan 2010 23:18:58 +0100 krauss new year's resolution: reindented code in function package
Fri, 11 Dec 2009 14:43:56 +0100 haftmann moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
Mon, 23 Nov 2009 15:05:59 +0100 krauss eliminated dead code and some unused bindings, reported by polyml
Thu, 19 Nov 2009 14:46:33 +0100 wenzelm adapted Local_Theory.define -- eliminated odd thm kind;
Fri, 13 Nov 2009 21:11:15 +0100 wenzelm modernized structure Local_Theory;
Fri, 13 Nov 2009 19:57:46 +0100 wenzelm inductive: eliminated obsolete kind;
Thu, 12 Nov 2009 22:02:11 +0100 wenzelm eliminated obsolete "internal" kind -- collapsed to unspecific "";
Fri, 30 Oct 2009 01:32:06 +0100 krauss less verbose inductive invocation
Fri, 30 Oct 2009 01:32:06 +0100 krauss tuned
Fri, 30 Oct 2009 01:32:06 +0100 krauss absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
Wed, 28 Oct 2009 16:25:27 +0100 wenzelm conceal internal bindings;
Fri, 23 Oct 2009 16:22:10 +0200 krauss function package: more standard names for structures and files
less more (0) tip