src/Pure/Isar/proof_context.ML
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
2006-11-30 wenzelm 2006-11-30 note_thmss: refrain from closing the derivation here;
2006-11-30 wenzelm 2006-11-30 removed obsolete (export_)standard;
2006-11-29 wenzelm 2006-11-29 *** bad commit -- reverted to previous version ***
2006-11-29 wenzelm 2006-11-29 removed export_standard_morphism; Assumption.assms_of: cterm;
2006-11-29 wenzelm 2006-11-29 removed export_standard_morphism;
2006-11-29 wenzelm 2006-11-29 removed export_standard_morphism; Assumption.assms_of: cterm;
2006-11-28 wenzelm 2006-11-28 simplified '?' operator; note_thmss: no naming;
2006-11-26 wenzelm 2006-11-26 added export_(standard_)morphism;
2006-11-21 wenzelm 2006-11-21 added stmt mode, which affects naming/indexing of local facts; renamed put_thms_internal to put_thms; notes: proper name and kind (outside of proof body); removed dead code;
2006-11-14 wenzelm 2006-11-14 replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
2006-11-09 wenzelm 2006-11-09 abbrevs: return result;
2006-11-07 wenzelm 2006-11-07 replaced const_syntax by notation, which operates on terms; read_const: include type;
2006-11-05 wenzelm 2006-11-05 added const_syntax_name;
2006-09-29 wenzelm 2006-09-29 Syntax.mode;
2006-09-19 wenzelm 2006-09-19 added standard;
2006-09-18 wenzelm 2006-09-18 pretty_thm: graceful treatment of ProtoPure.thy;
2006-08-09 wenzelm 2006-08-09 renamed map_theory to theory; added theory_result; prems_limit: default ~1;
2006-08-03 wenzelm 2006-08-03 tuned;
2006-08-02 wenzelm 2006-08-02 normalized Proof.context/method type aliases; simplified Assumption/ProofContext.export; prems_limit: < 0 means no output; added debug option (back from proof_display.ML);
2006-07-29 wenzelm 2006-07-29 rename legacy_pretty_thm to pretty_thm_legacy;
2006-07-27 wenzelm 2006-07-27 replaced extern_skolem by slightly more simplistic revert_skolems; moved fix_frees to variable.ML;
2006-07-27 wenzelm 2006-07-27 added legacy_pretty_thm (with fall-back on ProtoPure.thy); moved basic assumption operations to assumption.ML; tuned;
2006-07-26 wenzelm 2006-07-26 moved pprint functions to Isar/proof_display.ML; added primitive add_assumes; tuned internal prems: no names;
2006-07-19 wenzelm 2006-07-19 Sign.infer_types: Name.context; FactIndex.add_local: simplified interface; Variable.constraints_of;
2006-07-11 wenzelm 2006-07-11 adapted Name.defaults_of;
2006-07-11 wenzelm 2006-07-11 adapted to more efficient Name/Variable implementation; removed dead code;
2006-07-08 wenzelm 2006-07-08 Goal.prove: context;
2006-07-04 wenzelm 2006-07-04 print_lthms: include unnamed facts from index; tuned;
2006-07-04 wenzelm 2006-07-04 add_abbrevs/polymorphic: Variable.exportT_terms avoids over-generalization;