src/Pure/Isar/proof_context.ML
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;
2006-06-17 wenzelm 2006-06-17 export: simultaneous facts, refer to Variable.export; Term.internal/skolem;
2006-06-15 wenzelm 2006-06-15 ProofContext: moved variable operations to struct Variable;
2006-06-13 wenzelm 2006-06-13 tuned interfaces; added invent_types; added import_types/terms;
2006-06-12 wenzelm 2006-06-12 added declare_typ; simult_matches: Unify.matchers;
2006-06-11 wenzelm 2006-06-11 added import -- fixes schematic variables; added export;
2006-05-26 wenzelm 2006-05-26 removed unused extern_thm;
2006-05-17 wenzelm 2006-05-17 added CONST syntax; tuned interfaces;
2006-05-17 wenzelm 2006-05-17 always preserve authentic consts -- removed Syntax.mixfix_const;
2006-05-16 wenzelm 2006-05-16 export consts_of; added add_const_syntax; tuned interface;
2006-05-07 wenzelm 2006-05-07 removed 'concl is' patterns;
2006-05-02 wenzelm 2006-05-02 added set_syntax_mode, restore_syntax_mode;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-13 wenzelm 2006-04-13 expand_atom: Type.raw_match;
2006-04-11 wenzelm 2006-04-11 export pretty_classrel/arity;
2006-04-09 wenzelm 2006-04-09 added full_name; abbrevs: mode does not affect name space;
2006-04-08 wenzelm 2006-04-08 add_abbrevs(_i): support print mode; pretty_term': expand abbreviations only for well-typed terms; added expand_abbrevs; tuned;
2006-03-21 wenzelm 2006-03-21 subtract (op =); pretty_proof: no abbrevs;
2006-03-15 wenzelm 2006-03-15 rename_frees: treat trivial names; monomorphic: tuned invented names;
2006-03-14 wenzelm 2006-03-14 added monomorphic; export hidden_polymorphism;
2006-02-26 wenzelm 2006-02-26 put_thms: do_index;
2006-02-16 wenzelm 2006-02-16 added put_thms_internal: local_naming, no fact index; tuned;
2006-02-15 wenzelm 2006-02-15 replaced qualified_force_prefix to sticky_prefix; do not export read_terms;
2006-02-12 wenzelm 2006-02-12 consts: maintain thy version for efficient transfer; ins_sorts: Vartab.replace is slower than Vartab.update, but might avoid some copying of table structure;
2006-02-11 wenzelm 2006-02-11 added map_theory; added rename_frees; removed custom_accesses; added qualified_force_prefix; tuned local syntax;
2006-02-10 wenzelm 2006-02-10 tuned comment; moved local syntax to local_syntax.ML; common naming (for abbrevs and thms); transfer: merge consts; tuned pretty_term'; added polymorphic -- special case of generalize; added add_abbrevs(_i); read/cert: expand_consts;
2006-02-07 wenzelm 2006-02-07 added local consts component; tuned;
2006-02-06 wenzelm 2006-02-06 norm_term: Sign.const_expansion, Envir.expand_atom;
2006-02-06 haftmann 2006-02-06 subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate