src/HOL/Tools/Function/partial_function.ML
Wed, 27 Apr 2011 21:50:04 +0200 wenzelm clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
Mon, 18 Apr 2011 13:52:23 +0200 wenzelm standardized aliases of operations on tsig;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Thu, 24 Mar 2011 16:56:19 +0100 wenzelm added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
Sat, 08 Jan 2011 17:14:48 +0100 wenzelm misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
Mon, 13 Dec 2010 10:15:27 +0100 krauss eliminated dest_all_all_ctx
Tue, 26 Oct 2010 14:11:34 +0200 haftmann partial_function is a declaration command
less more (0) -7 tip