src/Pure/type.ML
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;
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-23 paulson 2009-09-23 Correct chasing of type variable instantiations during type unification. The following theory should not raise exception TERM: constdefs somepredicate :: "(('b => 'b) => ('a => 'a)) => 'a => 'b => bool" "somepredicate upd v x == True" lemma somepredicate_idI: "somepredicate id (f v) v" by (simp add: somepredicate_def) lemma somepredicate_triv: "somepredicate upd v x ==> somepredicate upd v x" by assumption lemmas somepredicate_triv [OF somepredicate_idI] lemmas st' = somepredicate_triv[where v="h :: nat => bool"] lemmas st2 = st'[OF somepredicate_idI]
2009-07-17 wenzelm 2009-07-17 eq_type: special case for empty environment;
2009-07-06 wenzelm 2009-07-06 witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;
2009-03-07 wenzelm 2009-03-07 replace old bstring by binding for logical primitives: class, type, const etc.;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm; use regular Term.add_XXX etc.;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-12-30 wenzelm 2008-12-30 varify: regular name context;
2008-12-05 haftmann 2008-12-05 dropped NameSpace.declare_base
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-08-27 wenzelm 2008-08-27 type Properties.T;
2008-06-21 wenzelm 2008-06-21 the_tags: explicit error message; new_decl: Position.thread_data;
2008-06-20 haftmann 2008-06-20 type constructors now with markup
2008-06-19 wenzelm 2008-06-19 add_abbrev: check tfrees of rhs, not tvars (addresses a lapse introduced in 1.65);
2008-04-15 wenzelm 2008-04-15 simplified hide_XXX interfaces;
2008-04-13 wenzelm 2008-04-13 tsig: removed unnecessary universal witness; Sorts.class_error: produce message only (formerly msg_class_error);
2008-04-02 haftmann 2008-04-02 canonical meet_sort operation
2008-03-19 haftmann 2008-03-19 Type.lookup now curried; typ_of_sort