src/Pure/type.ML
2015-03-31 wenzelm 2015-03-31 subtle change of long-standing name space policy: unknown entries are treated as hidden, consequently "private" is understood in the strict sense;
2015-03-31 wenzelm 2015-03-31 tuned signature;
2015-03-29 wenzelm 2015-03-29 tuned signature;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-08 wenzelm 2014-11-08 clarified name of Type.unified, to emphasize its connection to the "unify" family; tuned low-level operation;
2014-11-08 wenzelm 2014-11-08 recovered type matching, which was broken in 8a765db7e0f8 (see also 8a765db7e0f8, 2db1d3d2ed54); NB: "match" operates on direct substitution without variable chasing, in contrast to "unify" (and Unify.matches!) which work on cascaded env;
2014-03-13 wenzelm 2014-03-13 more frugal recording of changes: join merely requires information from one side; tuned;
2014-03-11 wenzelm 2014-03-11 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;
2014-03-11 wenzelm 2014-03-11 minor performance tuning via fast matching filter;
2014-03-10 wenzelm 2014-03-10 abstract type Name_Space.table; clarified pretty_locale_deps: sort strings; clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;
2014-03-09 wenzelm 2014-03-09 unused;
2014-03-06 wenzelm 2014-03-06 reject internal term names outright, and complete consts instead; more general Name_Space.check_reports; more compact Markup.markup_report;
2014-03-05 wenzelm 2014-03-05 more markup for inner syntax class/type names (notably for completion); explicit reports result without broadcast yet, which is important for brute-force disambiguation;
2014-03-02 wenzelm 2014-03-02 prefer Name_Space.check with its builtin reports (including completion);
2013-05-11 wenzelm 2013-05-11 prefer explicitly qualified exceptions, which is particular important for robust handlers;
2013-04-12 wenzelm 2013-04-12 tuned exceptions -- avoid composing error messages in low-level situations;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-03 wenzelm 2012-10-03 use explicit Type.strip_sorts_dummy to suppress sort constraints in output;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2012-03-18 wenzelm 2012-03-18 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
2012-02-24 wenzelm 2012-02-24 clarifed name space "type name", which covers logical and non-logical types, and often occurs inside outer syntax "type" markup;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-11-20 wenzelm 2011-11-20 clarified certify vs. sharing;
2011-11-10 wenzelm 2011-11-10 pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
2011-08-10 wenzelm 2011-08-10 avoid OldTerm operations -- with subtle changes of semantics;
2011-06-25 wenzelm 2011-06-25 entity markup for "type", "constant";
2011-06-25 wenzelm 2011-06-25 type classes: entity markup instead of old-style token markup;
2011-06-09 wenzelm 2011-06-09 simplified Name.variant -- discontinued builtin fold_map;
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2011-04-23 wenzelm 2011-04-23 clarified Type.the_decl;
2011-04-18 wenzelm 2011-04-18 pass plain Proof.context for pretty printing;
2011-04-18 wenzelm 2011-04-18 simplified Sorts.class_error: plain Proof.context; tuned;
2011-04-18 wenzelm 2011-04-18 simplified pretty printing context, which is only required for certain kernel operations; disentangled dependencies of structure Pretty;
2011-04-17 wenzelm 2011-04-17 added Binding.print convenience, which includes quote already;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2010-12-30 wenzelm 2010-12-30 uniform treatment of typ_match and raw_match (cf. b654fa27fbc4);
2010-12-17 wenzelm 2010-12-17 extra checking of name bindings for classes, types, consts; tuned;
2010-10-15 paulson 2010-10-15 prevention of self-referential type environments
2010-09-12 wenzelm 2010-09-12 Type_Infer.preterm: eliminated separate Constraint;
2010-09-12 wenzelm 2010-09-12 load type_infer.ML later -- proper context for Type_Infer.infer_types; renamed Type_Infer.polymorphicT to Type.mark_polymorphic;
2010-09-12 wenzelm 2010-09-12 common Type.appl_error, which also covers explicit constraints;
2010-09-12 wenzelm 2010-09-12 eliminated aliases of Type.constraint;
2010-05-04 wenzelm 2010-05-04 proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences: * present type variables are only compared wrt. first component (the atomic type), not the duplicated sort; * extra sorts are grounded towards fixed 'a, potentially with different sorts (the original version with Name.names could cause name clashes with other present variables, too, but this should not be a problem); * deriv_rule_unconditional ensures that proof terms are always maintained independently of the "proofs" flag -- this improves robustness and preserves basic PThm proofs required for extraction attributes, e.g. in theory HOL/Extraction;
2010-04-28 wenzelm 2010-04-28 more systematic naming of tsig operations;
2010-04-28 wenzelm 2010-04-28 export Type.minimize_sort;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-09 wenzelm 2010-03-09 aliases for class/type/const; tuned;
2010-03-09 wenzelm 2010-03-09 added ProofContext.tsig_of -- proforma version for local name space only, not logical content; added ProofContext.read_type_name_proper; localized ProofContext.read_class/read_arity/cert_arity; localized ProofContext.class_space/type_space etc.;
2010-02-25 wenzelm 2010-02-25 provide direct access to the different kinds of type declarations;
2010-01-05 haftmann 2010-01-05 avoid exporting Type.build_tsig
2009-12-02 haftmann 2009-12-02 exported build_tsig
2009-11-21 wenzelm 2009-11-21 explicitly mark some legacy freeze operations;
2009-11-09 wenzelm 2009-11-09 locale_const/target_notation: uniform use of Term.aconv_untyped; target_notation: pass on transformed term formally; removed obsolete Type.similar_types;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-10-25 wenzelm 2009-10-25 eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-24 wenzelm 2009-10-24 maintain position of formal entities via name space;
2009-10-24 wenzelm 2009-10-24 maintain explicit name space kind; export Name_Space.the_entry; tuned messages;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 wenzelm 2009-10-24 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already; simplified messages;