src/Provers/trancl.ML
Mon, 08 Jan 2018 16:45:30 +0100 wenzelm prefer qualified names;
Sun, 26 Jul 2015 17:32:59 +0200 wenzelm updated to infer_instantiate;
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, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Thu, 30 Oct 2014 22:45:19 +0100 wenzelm eliminated aliases;
Sun, 26 Feb 2012 21:43:57 +0100 haftmann dropped dead code
Wed, 08 Jun 2011 15:56:57 +0200 wenzelm more robust exception pattern General.Subscript;
Sat, 16 Apr 2011 18:11:20 +0200 wenzelm eliminated old List.nth;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Thu, 08 Jul 2010 16:19:24 +0200 haftmann tuned titles
Wed, 05 May 2010 18:25:34 +0200 haftmann farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
Mon, 22 Feb 2010 14:11:03 +0100 berghofe Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation
Thu, 22 Oct 2009 13:48:06 +0200 haftmann map_range (and map_index) combinator
Tue, 29 Sep 2009 23:19:26 +0200 wenzelm tuned;
less more (0) -15 tip