src/Pure/Isar/proof_context.ML
2007-10-16 wenzelm 2007-10-16 added revert_abbrev; contract_abbrevs: ignore Syntax.internalM (changed meaning of this special case); print_abbrevs: proper treatment of global consts (after local/global swap);
2007-10-15 haftmann 2007-10-15 swapped constant components
2007-10-11 wenzelm 2007-10-11 replaced Term.equiv_types by Type.similar_types;
2007-10-11 wenzelm 2007-10-11 moved ProofContext.pp to Syntax.pp;
2007-10-10 wenzelm 2007-10-10 generalized notation interface (add or del);
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations; proper installation of unparsers and term_uncheck (contract_abbrevs); removed obsolete pretty/string_of_term/typ/sort/classrel/arity (cf. structure Syntax); tuned;
2007-10-02 wenzelm 2007-10-02 export tsig_of;
2007-09-30 wenzelm 2007-09-30 add_abbrev: tags (Markup.property list);
2007-09-30 wenzelm 2007-09-30 standard_term_check: include expand_abbrevs (back again);
2007-09-29 wenzelm 2007-09-29 removed redundant const_constraint; add_const_constraint: proper certification; prepare_dummies: avoid imperative features; term_check: separate phases, standard_infer_types passes inference parameters instead of frees/vars; Syntax.install_operations: dummy unparsers;
2007-09-29 haftmann 2007-09-29 exported constraint interfaces
2007-09-24 wenzelm 2007-09-24 eliminated ProofContext.read_termTs;
2007-09-23 wenzelm 2007-09-23 removed dead code; tuned;
2007-09-23 wenzelm 2007-09-23 made smlnj happy;
2007-09-23 wenzelm 2007-09-23 added read_term_pattern/schematic/abbrev; prepare_patterns: Variable.polymorphic; removed obsolete cert/pats versions;
2007-09-22 wenzelm 2007-09-22 removed obsolete set_expand_abbrevs (superceded by mode_abbrev); pretty_term_abbrev: silently ignore ill-typed term; gen_bind: set_mode only locally;
2007-09-17 wenzelm 2007-09-17 avoid direct access to print_mode;
2007-09-01 wenzelm 2007-09-01 removed unused join_mode; standard_typ_check: proper prepare_patternT, which rejects schematic type vars in non-patterns;
2007-09-01 wenzelm 2007-09-01 removed obsolete read/cert variations (cf. Syntax.read/check);
2007-08-31 wenzelm 2007-08-31 reject_vars: accept type-inference params; standard_term_check: include prepare_pattern; infer_type: mode_schematic; tuned;
2007-08-31 wenzelm 2007-08-31 export various inner syntax modes; Syntax.add_term_check: include expand_abbrevs (consts and var bindings);
2007-08-30 wenzelm 2007-08-30 added join_mode; expand_binds: mode dependent; removed infer_types(_pat) -- use general Syntax.check_terms instead;
2007-08-30 wenzelm 2007-08-30 moved type_mode to type.ML; Syntax.add_typ_check;
2007-08-21 wenzelm 2007-08-21 added inner syntax mode, includes former type_mode and is_stmt;
2007-08-20 wenzelm 2007-08-20 inner syntax: added parse_term/prop;
2007-08-20 wenzelm 2007-08-20 prepare_dummies: NAMED_CRITICAL;
2007-08-14 wenzelm 2007-08-14 added implicit type mode (cf. Type.mode); added inner syntax parsers for sort/typ (no term/prop yet); infer_types: exception TYPE => error; read_vars: Syntax.parse_typ;
2007-07-27 wenzelm 2007-07-27 get_thm etc.: map empty name to dummy_thm;
2007-07-23 wenzelm 2007-07-23 marked some CRITICAL sections (for multithreading);
2007-06-13 wenzelm 2007-06-13 tuned msg;
2007-06-02 wenzelm 2007-06-02 moved specific target/local_abbrev to theory_target.ML;
2007-05-08 wenzelm 2007-05-08 simplified pretty_thm(_legacy);
2007-05-08 wenzelm 2007-05-08 legacy_intern_skolem: legacy_feature;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-23 wenzelm 2007-04-23 sane version of read_termTs (proper freeze); added read_terms, cert_terms;
2007-04-21 wenzelm 2007-04-21 added decode_term (belongs to Syntax module);
2007-04-18 wenzelm 2007-04-18 simplified ProofContext.infer_types(_pats);
2007-04-15 wenzelm 2007-04-15 replaced read_term_legacy by read_prop_legacy; read: intern_skolem before type-inference (many workarounds!); read: reject_tvars; removed obsolete TypeInfer.logicT -- use dummyT; add_fixes: not constraints for external names;
2007-04-15 wenzelm 2007-04-15 proper interface infer_types(_pat); Syntax.mixfixT; tuned;
2007-04-14 wenzelm 2007-04-14 Term.string_of_vname;
2007-04-14 wenzelm 2007-04-14 added Morphism.transform/form (generic non-sense);
2007-04-04 wenzelm 2007-04-04 renamed Output.has_mode to print_mode_active;
2007-02-26 wenzelm 2007-02-26 added theorems_of;
2007-02-23 haftmann 2007-02-23 add_path for naming in proof contexts
2006-12-13 wenzelm 2006-12-13 target_abbrev: internal mode for abbrevs; tuned;
2006-12-13 wenzelm 2006-12-13 local_abbrev: proper fix/declare of local entities;
2006-12-12 wenzelm 2006-12-12 add_abbrev: removed Assumption.add_assms (danger of inconsistent naming);
2006-12-12 wenzelm 2006-12-12 notation: Term.equiv_types; add_abbrev: tuned signature, added assumption export; added local_abbrev; tuned;
2006-12-11 wenzelm 2006-12-11 advanced translation functions: Proof.context;
2006-12-10 wenzelm 2006-12-10 removed junk;
2006-12-10 wenzelm 2006-12-10 added target_notation/abbrev; tuned;
2006-12-09 wenzelm 2006-12-09 added read/pretty_term_abbrev, print_abbrevs; tuned Consts signature; renamed expand_abbrevs to set_expand_abbrevs;
2006-12-07 wenzelm 2006-12-07 simplified add_abbrev -- single argument;
2006-12-07 wenzelm 2006-12-07 simplified add_abbrevs: no mixfix;
2006-12-07 wenzelm 2006-12-07 reorganized structure Goal vs. Tactic;
2006-12-06 wenzelm 2006-12-06 add_abbrevs: moved common parts to consts.ML;
2006-12-05 wenzelm 2006-12-05 add_notation: permissive about undeclared consts; add_abbrevs: allow qualified names; tuned;
2006-12-05 wenzelm 2006-12-05 more careful indexing of local facts;
2006-12-05 wenzelm 2006-12-05 note_thmss: added kind tag and non-official name;
2006-12-01 haftmann 2006-12-01 made SML/NJ happy