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
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;