src/Pure/type.ML
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
2007-11-10 wenzelm 2007-11-10 similar_types: uniform treatment of TFrees/TVars;
2007-11-07 wenzelm 2007-11-07 tuned signature;
2007-10-11 wenzelm 2007-10-11 replaced Term.equiv_types by Type.similar_types;
2007-10-04 wenzelm 2007-10-04 replaced literal 'a by Name.aT;
2007-08-30 wenzelm 2007-08-30 maintain mode in context (get/set/restore_mode);
2007-08-14 wenzelm 2007-08-14 type mode: models certification mode (default, syntax, abbrev); replaced certify_typ_syntax/abbrev by certify_typ_mode;
2007-07-08 wenzelm 2007-07-08 replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2006-12-29 wenzelm 2006-12-29 Sorts.minimal_classes;
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-10-31 haftmann 2006-10-31 fixed type signature of Type.varify
2006-10-10 haftmann 2006-10-10 gen_rem(s) abandoned in favour of remove / subtract
2006-09-21 wenzelm 2006-09-21 serial numbers for types;
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-06-07 wenzelm 2006-06-07 renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;
2006-05-22 wenzelm 2006-05-22 export raw_unifys, could_unifys;
2006-05-20 wenzelm 2006-05-20 export raw_matches;
2006-05-16 wenzelm 2006-05-16 more abstract interface to classes/arities;
2006-05-05 wenzelm 2006-05-05 replaced Sorts.DOMAIN by general Sorts.CLASS_ERROR; add_types etc.: reject qualified dummy types -- prevents users from messing up some internal conventions;
2006-05-02 wenzelm 2006-05-02 tuned;
2006-04-30 wenzelm 2006-04-30 build classes/arities: refer to operations in sorts.ML; simplified add_class/classrel/arity; tuned;
2006-04-25 wenzelm 2006-04-25 added inter_sort; added arity_number/sorts;
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality;
2006-03-11 wenzelm 2006-03-11 got rid of type Sign.sg;
2006-02-07 wenzelm 2006-02-07 renamed gen_duplicates to duplicates;
2006-02-06 wenzelm 2006-02-06 TableFun: renamed xxx_multi to xxx_list; tuned;
2006-02-06 haftmann 2006-02-06 subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
2005-10-08 wenzelm 2005-10-08 added could_unify;
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
2005-09-20 haftmann 2005-09-20 slight adaptions to library changes
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-08-29 wenzelm 2005-08-29 use AList operations;
2005-07-28 wenzelm 2005-07-28 typ_match, unify: canonical argument order; added raw_match, raw_instance; proper implementation of raw_unify;
2005-07-19 wenzelm 2005-07-19 tuned match, unify;
2005-07-01 berghofe 2005-07-01 Moved eq_type from envir.ML to type.ML
2005-06-17 wenzelm 2005-06-17 Symtab.fold;
2005-06-11 wenzelm 2005-06-11 name space of classes and types maintained in tsig;
2005-06-09 wenzelm 2005-06-09 renamed cert_typ_raw to cert_typ_abbrev; renamed add_abbrs to add_abbrevs; tuned;
2005-06-05 wenzelm 2005-06-05 added Type.freeze(_type); tuned;