src/Pure/type.ML
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;
Thu, 25 Feb 2010 22:05:34 +0100 wenzelm provide direct access to the different kinds of type declarations;
Tue, 05 Jan 2010 14:19:12 +0100 haftmann avoid exporting Type.build_tsig
Wed, 02 Dec 2009 17:53:35 +0100 haftmann exported build_tsig
Sat, 21 Nov 2009 15:49:29 +0100 wenzelm explicitly mark some legacy freeze operations;
Mon, 09 Nov 2009 20:47:39 +0100 wenzelm locale_const/target_notation: uniform use of Term.aconv_untyped;
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Sun, 25 Oct 2009 21:35:46 +0100 wenzelm eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
Sat, 24 Oct 2009 21:30:33 +0200 wenzelm maintain position of formal entities via name space;
Sat, 24 Oct 2009 20:54:08 +0200 wenzelm maintain explicit name space kind;
Sat, 24 Oct 2009 19:47:37 +0200 wenzelm renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
Sat, 24 Oct 2009 19:24:50 +0200 wenzelm eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
Wed, 30 Sep 2009 22:20:58 +0200 wenzelm eliminated redundant bindings;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Wed, 23 Sep 2009 11:05:28 +0100 paulson Correct chasing of type variable instantiations during type unification.
Fri, 17 Jul 2009 21:32:59 +0200 wenzelm eq_type: special case for empty environment;
Mon, 06 Jul 2009 22:41:00 +0200 wenzelm witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;
Sat, 07 Mar 2009 22:12:07 +0100 wenzelm replace old bstring by binding for logical primitives: class, type, const etc.;
Wed, 31 Dec 2008 18:53:19 +0100 wenzelm moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
Wed, 31 Dec 2008 15:30:10 +0100 wenzelm moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
Tue, 30 Dec 2008 21:48:07 +0100 wenzelm varify: regular name context;
Fri, 05 Dec 2008 08:04:53 +0100 haftmann dropped NameSpace.declare_base
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Wed, 27 Aug 2008 11:48:54 +0200 wenzelm type Properties.T;
Sat, 21 Jun 2008 16:18:50 +0200 wenzelm the_tags: explicit error message;
Fri, 20 Jun 2008 21:00:26 +0200 haftmann type constructors now with markup
less more (0) -100 -60 tip