src/Pure/Isar/theory_target.ML
2007-10-22 wenzelm 2007-10-22 tuned;
2007-10-22 haftmann 2007-10-22 tuned abbreviations in class context
2007-10-20 wenzelm 2007-10-20 tuned abbrev interface; PrintMode.internal;
2007-10-19 wenzelm 2007-10-19 internal tuning: class_target, fork_mixfix, declare_const (singleton), abbrev;
2007-10-19 haftmann 2007-10-19 clarified abbreviations in class context
2007-10-18 haftmann 2007-10-18 improved class syntax
2007-10-18 haftmann 2007-10-18 moved fork_mixfix to theory_target
2007-10-17 wenzelm 2007-10-17 tuned fork_mixfix (back from class.ML);
2007-10-16 haftmann 2007-10-16 clarified fork_mixfix
2007-10-16 wenzelm 2007-10-16 misc cleanup of abbrev/local_const;
2007-10-15 haftmann 2007-10-15 tuned
2007-10-14 wenzelm 2007-10-14 tuned various Class interfaces; tuned;
2007-10-13 wenzelm 2007-10-13 abbrev: return hypothetical def; replaced obsolete Theory.add_finals_i by Theory.add_deps; misc cleanup;
2007-10-12 wenzelm 2007-10-12 pass explicit target record -- more informative peek operation; removed obsolete hide_abbrev; misc tuning;
2007-10-12 haftmann 2007-10-12 tuned
2007-10-11 wenzelm 2007-10-11 local_axioms: impose hyps stemming from local consts as well (otherwise the axioms will be more general than expected!);
2007-10-11 wenzelm 2007-10-11 local_theory: incorporated consts into axioms; LocalDefs.expand_cterm; tuned;
2007-10-11 wenzelm 2007-10-11 replaced Term.equiv_types by Type.similar_types; moved add_axiom/def to more_thm.ML;
2007-10-11 wenzelm 2007-10-11 replaced Sign.add_consts_authentic by Sign.declare_const;
2007-10-10 wenzelm 2007-10-10 generalized notation interface (add or del);
2007-10-09 wenzelm 2007-10-09 tuned;
2007-10-09 wenzelm 2007-10-09 removed LocalTheory.defs/target_morphism operations; moved target_morphism to local_theory.ML; renamed init_i to init, and init to init_cmd; tuned;
2007-10-08 haftmann 2007-10-08 added proper subclass concept; improved class target
2007-10-08 wenzelm 2007-10-08 primitive add_def: strip sorts in axiom;
2007-10-08 haftmann 2007-10-08 added first version of user-space type system for class target
2007-10-04 wenzelm 2007-10-04 replaced literal 'a by Name.aT;
2007-10-04 haftmann 2007-10-04 put declarations first
2007-10-02 wenzelm 2007-10-02 added add_defs_new, which strips sorts for axioms (presently inactive);
2007-09-30 wenzelm 2007-09-30 keep context position as tags for consts/thms;
2007-09-29 haftmann 2007-09-29 proper syntax during class specification
2007-09-20 haftmann 2007-09-20 fixed wrong syntax treatment in class target
2007-08-21 wenzelm 2007-08-21 ProofContext.restore_mode;
2007-08-17 haftmann 2007-08-17 dropped junk
2007-08-10 haftmann 2007-08-10 ClassPackage renamed to Class
2007-06-02 wenzelm 2007-06-02 added target/local_abbrev (from proof_context.ML); target_abbrev: demand equal head const (tool compliance);
2007-05-24 haftmann 2007-05-24 rudimentary class target implementation
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-15 wenzelm 2007-04-15 proper ProofContext.infer_types;
2007-04-14 wenzelm 2007-04-14 declarations: apply target_morphism;
2007-03-09 haftmann 2007-03-09 *** empty log message ***
2007-02-28 wenzelm 2007-02-28 abbrev: be permissive after transformation;
2007-02-23 haftmann 2007-02-23 tuned
2007-02-10 haftmann 2007-02-10 added class target stub
2007-01-28 wenzelm 2007-01-28 added interface for target_naming;
2006-12-14 wenzelm 2006-12-14 defs/notes: more robust transitivity reasoning;
2006-12-13 wenzelm 2006-12-13 internal_abbrev: observe print mode;
2006-12-12 wenzelm 2006-12-12 tuned;
2006-12-12 wenzelm 2006-12-12 removed is_class -- handled internally; begin: is_class argument; added fork_mixfix; abbrev/defs: internal_abbrev produces hypothetical term;
2006-12-10 wenzelm 2006-12-10 defs: increased entropy of mixfix handling;
2006-12-10 wenzelm 2006-12-10 removed junk;
2006-12-10 wenzelm 2006-12-10 added is_class (approximation); added abbrev; tuned;
2006-12-09 wenzelm 2006-12-09 TermSyntax.abbrev;
2006-12-07 wenzelm 2006-12-07 reorganized structure Tactic vs. MetaSimplifier;
2006-12-07 wenzelm 2006-12-07 TermSyntax.notation/abbrevs;
2006-12-05 wenzelm 2006-12-05 target_name: allow qualified names;
2006-12-05 wenzelm 2006-12-05 notes: added non-official name;
2006-11-30 wenzelm 2006-11-30 notes: proper naming of thm proof, activated import_export_proof;
2006-11-30 wenzelm 2006-11-30 notes: more careful treatment of Goal.close_result; tuned;
2006-11-30 wenzelm 2006-11-30 notes: proper import/export of proofs (still inactive); Goal.norm/close_result; tuned;
2006-11-29 wenzelm 2006-11-29 reworked notes: towards proper import/export of proof terms; tuned;