src/FOLP/simp.ML
Fri, 15 Oct 2021 19:25:31 +0200 wenzelm discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
Sat, 02 Oct 2021 12:04:14 +0200 wenzelm proper term operation Term.dest_abs;
Sun, 12 Sep 2021 20:24:14 +0200 wenzelm more antiquotations;
Wed, 07 Aug 2019 10:31:54 +0200 wenzelm more careful treatment of implicit context;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Fri, 25 Sep 2015 20:37:59 +0200 wenzelm moved remaining display.ML to more_thm.ML;
Sun, 26 Jul 2015 21:50:44 +0200 wenzelm updated to infer_instantiate;
Sun, 26 Jul 2015 21:48:00 +0200 wenzelm proper context;
Fri, 24 Jul 2015 22:16:39 +0200 wenzelm proper context;
Sat, 18 Jul 2015 21:25:55 +0200 wenzelm prefer tactics with explicit context;
Sat, 18 Jul 2015 20:54:56 +0200 wenzelm prefer tactics with explicit context;
Sun, 05 Jul 2015 19:08:40 +0200 wenzelm clarified context;
Sun, 05 Jul 2015 16:44:59 +0200 wenzelm eliminated spurious warning/tracing messages -- avoid Display.string_of_thm_without_context;
Sun, 05 Jul 2015 16:39:25 +0200 wenzelm clarified context;
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.;
Sun, 21 Dec 2014 22:49:17 +0100 wenzelm tuned signature;
Mon, 10 Nov 2014 21:49:48 +0100 wenzelm proper context for assume_tac (atac remains as fall-back without context);
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy;
Sat, 16 Apr 2011 18:11:20 +0200 wenzelm eliminated old List.nth;
Fri, 08 Apr 2011 13:31:16 +0200 wenzelm explicit structure Syntax_Trans;
Sat, 15 May 2010 21:50:05 +0200 wenzelm less pervasive names from structure Thm;
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 =)
Fri, 30 Apr 2010 23:53:37 +0200 wenzelm renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Thu, 29 Oct 2009 23:56:33 +0100 wenzelm eliminated some old folds;
Thu, 29 Oct 2009 17:58:26 +0100 wenzelm standardized filter/filter_out;
less more (0) -50 -30 tip