src/Pure/unify.ML
Sun, 25 Feb 2018 19:43:38 +0100 wenzelm prefer symbols;
Sun, 25 Feb 2018 15:44:46 +0100 wenzelm eliminated ASCII syntax from Pure bootstrap;
Tue, 13 Dec 2016 11:51:42 +0100 wenzelm more symbols;
Fri, 21 Nov 2014 18:14:39 +0100 wenzelm removed some add-ons from modules that are relevant for the inference kernel;
Sat, 08 Nov 2014 21:31:51 +0100 wenzelm optional proof context for unify operations, for the sake of proper local options;
Sun, 06 Apr 2014 16:36:28 +0200 wenzelm more source positions;
Wed, 26 Mar 2014 14:41:52 +0100 wenzelm prefer Context_Position where a context is available;
Thu, 18 Jul 2013 22:00:35 +0200 wenzelm guard unify tracing via visible status of global theory;
Thu, 18 Jul 2013 21:06:21 +0200 wenzelm tuned;
Wed, 29 May 2013 12:03:58 +0200 wenzelm tuned signature;
Wed, 29 May 2013 11:53:31 +0200 wenzelm backout 3b9c31867707 -- too risky to "amend" modules from 25 years ago that don't handle Vars with different types;
Mon, 27 May 2013 16:52:39 +0200 wenzelm more thorough type unification: treat equal Vars like other atoms, otherwise unify type of term pair (not just accidental body_type of its head Vars);
Fri, 24 May 2013 15:13:25 +0200 wenzelm tuned signature -- slightly more general operations (cf. term.ML);
Fri, 24 May 2013 14:31:44 +0200 wenzelm re-use Pattern.unify_types, including its trace_unify_fail option;
Fri, 24 May 2013 14:00:10 +0200 wenzelm tuned signature;
Fri, 12 Apr 2013 14:54:14 +0200 wenzelm tuned signature;
Sun, 15 Jul 2012 17:53:47 +0200 wenzelm prefer canonical fold_rev;
Sun, 15 Jul 2012 17:27:19 +0200 wenzelm back to naive insertion sort before 1997 to accommodate peculiar less_arg relation -- NB: make_ord arg_less was not a quasi-order and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
Sat, 14 Jan 2012 21:16:15 +0100 wenzelm discontinued old-style Term.list_abs in favour of plain Term.abs;
Thu, 07 Apr 2011 21:23:57 +0200 wenzelm constant =?= no longer exists (cf. 8c09e1fa24a7);
Thu, 30 Dec 2010 22:34:53 +0100 wenzelm uniform treatment of type vs. term environment (cf. b654fa27fbc4);
Fri, 15 Oct 2010 17:21:07 +0100 paulson prevention of self-referential type environments
Mon, 06 Sep 2010 21:33:19 +0200 wenzelm more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
Fri, 03 Sep 2010 16:09:12 +0200 wenzelm more explicit Config.declare vs. Config.declare_global;
Mon, 05 Jul 2010 14:21:30 +0100 paulson Unification (flexflex) bug fix; making "auto" deterministic
Tue, 29 Jun 2010 22:59:29 +0200 wenzelm fail with low-level exception, not user error;
Tue, 29 Jun 2010 21:56:31 +0200 wenzelm eliminated some unused bindings;
Tue, 29 Jun 2010 21:46:47 +0200 wenzelm recovered some indentation from the depths of time;
Mon, 10 May 2010 20:53:06 +0200 wenzelm renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
Sun, 28 Mar 2010 16:59:06 +0200 wenzelm static defaults for configuration options;
less more (0) -50 -30 tip