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-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-29 wenzelm 2010-04-29 read_const: disallow internal names as usual in visible Isar text;
2010-04-29 wenzelm 2010-04-29 ProofContext.read_const: allow for type constraint (for fixed variable); added proof command 'write' to introduce concrete syntax within a proof body;
2010-04-29 wenzelm 2010-04-29 allow mixfix syntax for fixes within a proof body -- should now work thanks to fully authentic syntax;
2010-04-28 wenzelm 2010-04-28 localized default sort;
2010-04-28 wenzelm 2010-04-28 more systematic naming of tsig operations;
2010-04-28 wenzelm 2010-04-28 get_sort: minimize sorts given in the text, while keeping those from the context unchanged (the latter are preferred); tuned;
2010-04-27 wenzelm 2010-04-27 monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
2010-04-15 wenzelm 2010-04-15 get_sort: suppress dummyS from input; added check_tvar, check_tfree convenience; tuned;
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-03-06 wenzelm 2010-03-06 provide ProofContext.def_type depending on "pattern" mode;
2010-03-03 wenzelm 2010-03-03 authentic syntax for classes and type constructors; read/intern formal entities just after raw parsing, extern just before final pretty printing; discontinued _class token translation; moved Local_Syntax.extern_term to Syntax/printer.ML; misc tuning;
2010-03-01 wenzelm 2010-03-01 more uniform treatment of syntax for types vs. consts;
2010-02-27 wenzelm 2010-02-27 clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
2010-02-25 wenzelm 2010-02-25 clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
2010-02-21 wenzelm 2010-02-21 slightly more abstract syntax mark/unmark operations;
2010-02-21 wenzelm 2010-02-21 authentic syntax for *all* term constants;
2010-02-18 berghofe 2010-02-18 Use top-down rewriting to contract abbreviations.
2010-02-16 wenzelm 2010-02-16 simplified meaning of ProofContext.verbose; eliminated strange ProofContext.setmp_verbose_CRITICAL; less confusing printing of (cumulative) unnamed facts;
2010-02-16 wenzelm 2010-02-16 misc tuning and simplification;
2010-02-15 wenzelm 2010-02-15 discontinued unnamed infix syntax;
2010-02-11 wenzelm 2010-02-11 added ML antiquotation @{syntax_const};
2010-02-02 blanchet 2010-02-02 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-15 wenzelm 2009-11-15 eliminated obsolete thm position tags;
2009-11-12 wenzelm 2009-11-12 eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
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-11-02 wenzelm 2009-11-02 modernized structure Local_Syntax;
2009-11-02 wenzelm 2009-11-02 modernized structure AutoBind;
2009-11-02 wenzelm 2009-11-02 modernized structure Context_Position;
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-27 wenzelm 2009-10-27 ProofContext.setmp_verbose_CRITICAL;
2009-10-25 wenzelm 2009-10-25 eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25 wenzelm 2009-10-25 more direct access to naming; tuned signature;
2009-10-25 wenzelm 2009-10-25 allow name space entries to be "concealed" -- via binding/naming/local_theory;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-20 wenzelm 2009-10-20 backpatching of structure Proof and ProofContext -- avoid odd aliases; renamed transfer_proof to raw_transfer; indicate firm naming conventions for theory, Proof.context, Context.generic;
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-21 wenzelm 2009-07-21 moved ProofContext.pretty_thm to Display.pretty_thm etc.; explicit old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.; removed some very old thm print operations;
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir operations;
2009-07-14 wenzelm 2009-07-14 tuned prepare_patternT: Term.exists_subtype;
2009-03-31 wenzelm 2009-03-31 tuned error message;
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-28 wenzelm 2009-03-28 tuned;
2009-03-28 wenzelm 2009-03-28 replaced add_binds(_i) by bind_terms -- internal version only;
2009-03-26 wenzelm 2009-03-26 pretty_thm_aux etc.: explicit show_status flag;
2009-03-21 wenzelm 2009-03-21 removed obsolete pprint operations; some explicit pp operations for toplevel pretty printing;
2009-03-19 wenzelm 2009-03-19 use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
2009-03-18 wenzelm 2009-03-18 de-camelized Symbol_Pos;
2009-03-17 wenzelm 2009-03-17 reverted abbreviations: improved performance via Item_Net.T;
2009-03-12 wenzelm 2009-03-12 Assumption.all_prems_of, Assumption.all_assms_of;
2009-03-12 wenzelm 2009-03-12 renamed sticky_prefix to mandatory_path;
2009-03-11 wenzelm 2009-03-11 eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);