2015-09-24 wenzelm 2015-09-24 more explicit Defs.context: use proper name spaces as far as possible;
2015-09-23 wenzelm 2015-09-23 tuned signature;
2015-09-22 wenzelm 2015-09-22 eliminated separate type Theory.dep: use typeargs uniformly for consts/types; Object_Logic.add_judgment more like Theory.specify_const;
2015-09-22 wenzelm 2015-09-22 clarified deps entry: global names for arguments;
2015-09-22 wenzelm 2015-09-22 tuned whitespace;
2015-09-22 wenzelm 2015-09-22 HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015; defs.ML: track dependencies also for type constructors; typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type; Pure types and typedecls are final -- no dependencies;
2015-04-08 wenzelm 2015-04-08 proper context for Object_Logic operations;
2014-05-12 wenzelm 2014-05-12 tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";
2014-03-26 wenzelm 2014-03-26 prefer Context_Position where a context is available; prefer explicit Context_Position.is_visible -- avoid redundant message composition; tuned signature;
2013-04-10 wenzelm 2013-04-10 more standard module name Axclass (according to file name);
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;
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 modernized structure Proof_Context;
2010-08-27 wenzelm 2010-08-27 more careful treatment of context visibility flag wrt. spurious warnings;
2010-08-26 wenzelm 2010-08-26 renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
2010-08-12 haftmann 2010-08-12 Named_Target.theory_init
2010-08-11 haftmann 2010-08-11 renamed Theory_Target to the more appropriate Named_Target
2010-04-28 wenzelm 2010-04-28 tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
2010-04-16 wenzelm 2010-04-16 replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix); misc tuning and simplification;
2010-04-16 wenzelm 2010-04-16 allow syntax types within abbreviations;
2010-04-16 wenzelm 2010-04-16 local type abbreviations;
2010-04-15 wenzelm 2010-04-15 explicit ProofContext.check_tfree;
2010-04-15 wenzelm 2010-04-15 replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions =; simplified via ProofContext.check_tfree;
2010-03-19 wenzelm 2010-03-19 support type arguments with sort constraints;
2010-03-18 wenzelm 2010-03-18 eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types); allow sort constraints; misc tuning and clarification;
2010-03-13 wenzelm 2010-03-13 added typedecl_wrt, which affects default sorts of type args; misc tuning and simplification;
2010-03-11 wenzelm 2010-03-11 actually apply morphism to binding;
2010-03-09 wenzelm 2010-03-09 localized typedecl;
2010-03-07 wenzelm 2010-03-07 separate structure Typedecl;