src/HOL/Prolog/prolog.ML
Sat, 05 Jan 2019 17:24:33 +0100 wenzelm isabelle update -u control_cartouches;
Sat, 18 Jul 2015 20:54:56 +0200 wenzelm prefer tactics with explicit context;
Thu, 19 Mar 2015 22:30:57 +0100 wenzelm more position information;
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.;
Tue, 08 Apr 2014 14:59:36 +0200 wenzelm more uniform ML/document antiquotations;
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Sun, 26 Jan 2014 13:45:40 +0100 wenzelm tuned signature;
Sat, 25 Jan 2014 22:06:07 +0100 wenzelm explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
Thu, 30 May 2013 13:20:04 +0200 wenzelm tuned;
Mon, 20 May 2013 18:37:35 +0200 wenzelm proper run-time context;
Thu, 16 May 2013 21:48:01 +0200 wenzelm more system options as context-sensitive config options;
Tue, 14 Feb 2012 21:45:32 +0100 wenzelm more conventional tactic setup;
Mon, 09 Jan 2012 18:29:42 +0100 wenzelm prefer antiquotations;
Sun, 27 Nov 2011 23:10:19 +0100 wenzelm more antiquotations;
Thu, 24 Nov 2011 21:01:06 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Fri, 03 Sep 2010 21:13:53 +0200 wenzelm pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
Fri, 27 Aug 2010 14:07:09 +0200 wenzelm expanded some aliases from structure Unsynchronized;
Fri, 27 Aug 2010 10:56:46 +0200 haftmann formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
Thu, 26 Aug 2010 20:51:17 +0200 haftmann formerly unnamed infix impliciation now named HOL.implies
Thu, 19 Aug 2010 16:08:54 +0200 haftmann more antiquotations
Thu, 19 Aug 2010 11:02:14 +0200 haftmann use antiquotations for remaining unqualified constants in HOL
Sat, 15 May 2010 21:50:05 +0200 wenzelm less pervasive names from structure Thm;
Fri, 19 Feb 2010 16:11:45 +0100 wenzelm renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
Thu, 15 Oct 2009 23:28:10 +0200 wenzelm replaced String.concat by implode;
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Thu, 30 Jul 2009 12:20:43 +0200 wenzelm qualified Subgoal.FOCUS;
Thu, 30 Jul 2009 11:23:57 +0200 wenzelm FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;
Tue, 28 Jul 2009 20:03:58 +0200 wenzelm eliminated METAHYPS;
Wed, 15 Jul 2009 23:48:21 +0200 wenzelm more antiquotations;
Mon, 16 Jun 2008 22:13:39 +0200 wenzelm pervasive RuleInsts;
Mon, 16 Jun 2008 17:54:42 +0200 wenzelm ptac/prolog_tac: proper context;
Wed, 11 Jun 2008 18:02:00 +0200 wenzelm Drule.read_instantiate;
Mon, 20 Nov 2006 21:23:12 +0100 wenzelm HOL-Prolog: converted legacy ML scripts;
less more (0) tip