2015-07-09 wenzelm 2015-07-09 SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
2015-07-08 wenzelm 2015-07-08 Variable.focus etc.: optional bindings provided by user; Subgoal.focus command: more careful treatment of user-provided bindings;
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-06-09 wenzelm 2015-06-09 clarified term bindings;
2015-06-03 wenzelm 2015-06-03 clarified context;
2015-03-31 wenzelm 2015-03-31 tuned signature;
2015-03-31 wenzelm 2015-03-31 tuned signature;
2015-03-29 wenzelm 2015-03-29 tuned signature;
2015-03-28 wenzelm 2015-03-28 prefer Variable.focus, despite subtle differences of Logic.strip_params vs. Term.strip_all_vars;
2015-03-24 wenzelm 2015-03-24 tuned;
2015-03-24 wenzelm 2015-03-24 admit dummy patterns in instantiations; clarified context;
2015-03-23 wenzelm 2015-03-23 implicit goal parameters are improper;
2015-03-07 wenzelm 2015-03-07 added declare_maxidx operations for Eisbach;
2015-03-07 wenzelm 2015-03-07 clarified Variable.export: observe maxidx of target context;
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-05 wenzelm 2015-03-05 tuned -- more explicit use of context;
2014-12-21 wenzelm 2014-12-21 tuned signature;
2014-12-19 wenzelm 2014-12-19 tuned;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-10-13 wenzelm 2014-10-13 tuned signature;
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-06 wenzelm 2014-03-06 tuned signature;
2014-02-20 wenzelm 2014-02-20 tuned signature; tuned message;
2014-01-15 wenzelm 2014-01-15 general notion of auxiliary bounds within context; revert_bounds as part of regular unparse_term; avoid special variants of Syntax.string_of_term in Simplifier (e.g. relevant for add-on tracing);
2013-12-13 wenzelm 2013-12-13 maintain morphism names for diagnostic purposes;
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 tuned;
2012-10-03 wenzelm 2012-10-03 allow position constraints to coexist with 0 or 1 sort constraints; more position information in sorting error; report sorting of all type variables;
2012-10-01 wenzelm 2012-10-01 report sort assignment of visible type variables;
2012-03-19 wenzelm 2012-03-19 clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);
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-03-11 wenzelm 2012-03-11 more direct Name_Space.defined_entry; tuned Variable.export_inst: avoid keeping full contexts within the gen_fixesT closure (NB: locale infrastructure stores morphisms persistently);
2012-02-15 wenzelm 2012-02-15 renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-11-27 wenzelm 2011-11-27 tuned;
2011-11-12 wenzelm 2011-11-12 tuned markup -- prefer user-perspective;
2011-11-11 wenzelm 2011-11-11 discontinued entity text color, notably historic red for classes; tuned entity names;
2011-11-09 wenzelm 2011-11-09 tuned;
2011-11-07 wenzelm 2011-11-07 tuned;
2011-10-28 wenzelm 2011-10-28 slightly more explicit/syntactic modelling of morphisms;
2011-07-12 wenzelm 2011-07-12 more thorough Variable.check_name: Binding.check for logical entities within the term language;
2011-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2011-06-09 wenzelm 2011-06-09 simplified Name.variant -- discontinued builtin fold_map;
2011-04-27 wenzelm 2011-04-27 clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
2011-04-27 wenzelm 2011-04-27 tuned signature -- eliminated odd comment;
2011-04-27 wenzelm 2011-04-27 more informative markup for fixed variables (via name space entry); uniform markup for undeclared entities; tuned;
2011-04-27 wenzelm 2011-04-27 reorganized fixes as specialized (global) name space;
2011-04-27 wenzelm 2011-04-27 more uniform Variable.add_frees/add_fixed etc.;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 tuned signature, disentangled dependencies;
2010-10-25 wenzelm 2010-10-25 recovered some odd two-dimensional layout;
2010-09-24 wenzelm 2010-09-24 modernized structure Ord_List;
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-08-27 wenzelm 2010-08-27 more careful treatment of context visibility flag wrt. spurious warnings;
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-04 wenzelm 2010-05-04 simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-30 wenzelm 2010-04-30 renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop