src/Pure/type.ML
Wed, 06 Dec 2023 15:58:20 +0100 wenzelm clarified modules;
Tue, 05 Dec 2023 20:56:51 +0100 wenzelm misc tuning and clarification;
Sat, 06 May 2023 23:20:20 +0200 wenzelm back to more elementary concept of aliases as adhoc change of accesses, but now with "suppress" information (see also 31ea5c1f874d);
Fri, 05 May 2023 15:56:12 +0200 wenzelm more explicit entries for aliases, with proper checks in "strict" mode (e.g. for logical entities);
Sat, 02 Oct 2021 12:59:16 +0200 wenzelm clarified signature;
Thu, 09 Sep 2021 12:33:14 +0200 wenzelm clarified signature;
Sat, 04 Sep 2021 22:05:35 +0200 wenzelm clarified signature;
Sat, 04 Sep 2021 21:45:43 +0200 wenzelm more scalable operations;
Sat, 04 Sep 2021 21:25:08 +0200 wenzelm clarified signature;
Mon, 03 Jul 2017 09:12:13 +0200 wenzelm unused;
Fri, 25 Sep 2015 19:13:47 +0200 wenzelm tuned signature: eliminated pointless type Context.pretty;
Tue, 31 Mar 2015 21:12:22 +0200 wenzelm subtle change of long-standing name space policy: unknown entries are treated as hidden, consequently "private" is understood in the strict sense;
Tue, 31 Mar 2015 20:18:10 +0200 wenzelm tuned signature;
Sun, 29 Mar 2015 19:24:07 +0200 wenzelm tuned signature;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Sat, 08 Nov 2014 17:39:01 +0100 wenzelm clarified name of Type.unified, to emphasize its connection to the "unify" family;
Sat, 08 Nov 2014 15:01:05 +0100 wenzelm recovered type matching, which was broken in 8a765db7e0f8 (see also 8a765db7e0f8, 2db1d3d2ed54);
Thu, 13 Mar 2014 17:26:22 +0100 wenzelm more frugal recording of changes: join merely requires information from one side;
Tue, 11 Mar 2014 22:49:28 +0100 wenzelm more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
Tue, 11 Mar 2014 10:14:45 +0100 wenzelm minor performance tuning via fast matching filter;
Mon, 10 Mar 2014 13:55:03 +0100 wenzelm abstract type Name_Space.table;
Sun, 09 Mar 2014 17:43:40 +0100 wenzelm unused;
Thu, 06 Mar 2014 16:12:26 +0100 wenzelm reject internal term names outright, and complete consts instead;
Wed, 05 Mar 2014 18:26:35 +0100 wenzelm more markup for inner syntax class/type names (notably for completion);
Sun, 02 Mar 2014 21:02:27 +0100 wenzelm prefer Name_Space.check with its builtin reports (including completion);
Sat, 11 May 2013 16:57:18 +0200 wenzelm prefer explicitly qualified exceptions, which is particular important for robust handlers;
Fri, 12 Apr 2013 15:30:38 +0200 wenzelm tuned exceptions -- avoid composing error messages in low-level situations;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Wed, 03 Oct 2012 16:42:36 +0200 wenzelm use explicit Type.strip_sorts_dummy to suppress sort constraints in output;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
Fri, 24 Feb 2012 18:14:06 +0100 wenzelm clarifed name space "type name", which covers logical and non-logical types, and often occurs inside outer syntax "type" markup;
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Sun, 20 Nov 2011 15:21:22 +0100 wenzelm clarified certify vs. sharing;
Thu, 10 Nov 2011 22:32:10 +0100 wenzelm pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
Wed, 10 Aug 2011 19:21:28 +0200 wenzelm avoid OldTerm operations -- with subtle changes of semantics;
Sat, 25 Jun 2011 19:38:35 +0200 wenzelm entity markup for "type", "constant";
Sat, 25 Jun 2011 18:15:36 +0200 wenzelm type classes: entity markup instead of old-style token markup;
Thu, 09 Jun 2011 17:51:49 +0200 wenzelm simplified Name.variant -- discontinued builtin fold_map;
Thu, 09 Jun 2011 16:34:49 +0200 wenzelm discontinued Name.variant to emphasize that this is old-style / indirect;
Sat, 23 Apr 2011 18:25:50 +0200 wenzelm clarified Type.the_decl;
Mon, 18 Apr 2011 13:26:39 +0200 wenzelm pass plain Proof.context for pretty printing;
Mon, 18 Apr 2011 12:04:21 +0200 wenzelm simplified Sorts.class_error: plain Proof.context;
Mon, 18 Apr 2011 11:13:29 +0200 wenzelm simplified pretty printing context, which is only required for certain kernel operations;
Sun, 17 Apr 2011 21:42:47 +0200 wenzelm added Binding.print convenience, which includes quote already;
Sun, 17 Apr 2011 19:54:04 +0200 wenzelm report Name_Space.declare/define, relatively to context;
Sat, 16 Apr 2011 13:48:45 +0200 wenzelm Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
Thu, 30 Dec 2010 22:07:18 +0100 wenzelm uniform treatment of typ_match and raw_match (cf. b654fa27fbc4);
Fri, 17 Dec 2010 22:23:56 +0100 wenzelm extra checking of name bindings for classes, types, consts;
Fri, 15 Oct 2010 17:21:07 +0100 paulson prevention of self-referential type environments
Sun, 12 Sep 2010 22:28:59 +0200 wenzelm Type_Infer.preterm: eliminated separate Constraint;
Sun, 12 Sep 2010 20:47:47 +0200 wenzelm load type_infer.ML later -- proper context for Type_Infer.infer_types;
Sun, 12 Sep 2010 19:55:45 +0200 wenzelm common Type.appl_error, which also covers explicit constraints;
Sun, 12 Sep 2010 19:04:02 +0200 wenzelm eliminated aliases of Type.constraint;
Tue, 04 May 2010 14:38:59 +0200 wenzelm proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
Wed, 28 Apr 2010 11:13:11 +0200 wenzelm more systematic naming of tsig operations;
Wed, 28 Apr 2010 10:43:08 +0200 wenzelm export Type.minimize_sort;
Sat, 20 Mar 2010 17:33:11 +0100 wenzelm renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
Tue, 09 Mar 2010 23:29:04 +0100 wenzelm aliases for class/type/const;
Tue, 09 Mar 2010 14:35:02 +0100 wenzelm added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
less more (0) -100 -60 tip