src/HOL/Tools/Function/measure_functions.ML
Wed, 06 Dec 2017 20:43:09 +0100 wenzelm prefer control symbol antiquotations;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Tue, 03 Mar 2015 19:08:04 +0100 traytel eliminated some clones of Proof_Context.cterm_of
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Sat, 16 Aug 2014 19:20:11 +0200 wenzelm updated to named_theorems;
Fri, 07 Mar 2014 14:21:15 +0100 blanchet tuning
less more (0) -10 -7 tip