src/Pure/Isar/class_target.ML
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
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-02-23 haftmann 2010-02-23 dropped axclass
2010-02-15 haftmann 2010-02-15 clarifed type
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-30 haftmann 2009-11-30 dropped some unused bindings
2009-11-30 haftmann 2009-11-30 more accurate linerarity
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-10-25 wenzelm 2009-10-25 eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-17 wenzelm 2009-10-17 operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-10-01 haftmann 2009-10-01 proper merge of interpretation equations
2009-10-01 ballarin 2009-10-01 Merged.
2009-08-19 ballarin 2009-08-19 Improved comments and api names.
2009-08-15 haftmann 2009-08-15 additional checkpoints avoid problems in error situations
2009-07-15 haftmann 2009-07-15 simplification of locale interfaces
2009-07-10 haftmann 2009-07-10 tuned locale interface
2009-06-29 haftmann 2009-06-29 mutual instances
2009-06-17 haftmann 2009-06-17 stripped dead comment
2009-06-14 haftmann 2009-06-14 axclass command now legacy
2009-06-09 haftmann 2009-06-09 tuned make/map/merge combinators
2009-05-24 haftmann 2009-05-24 tuned class user space type system code
2009-05-20 haftmann 2009-05-20 tuned
2009-05-20 haftmann 2009-05-20 avoid potential problem with stale theory
2009-04-28 haftmann 2009-04-28 prevent potential failure
2009-03-28 wenzelm 2009-03-28 simplified Locale.activate operations, using generic context; misc tuning;
2009-03-13 wenzelm 2009-03-13 merged
2009-03-13 haftmann 2009-03-13 coherent binding policy with primitive target operations
2009-03-13 wenzelm 2009-03-13 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-07 wenzelm 2009-03-07 more uniform handling of binding in targets and derived elements;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-02-18 haftmann 2009-02-18 more precise improvement in instantiation user space type system
2009-01-26 haftmann 2009-01-26 fixed reading of class specs: declare class operations in context
2009-01-21 haftmann 2009-01-21 allow empty class specs
2009-01-21 haftmann 2009-01-21 code cleanup
2009-01-19 haftmann 2009-01-19 improved tackling of subclasses
2009-01-17 haftmann 2009-01-17 tuned signature
2009-01-17 haftmann 2009-01-17 code cleanup
2009-01-16 haftmann 2009-01-16 migrated class package to new locale implementation
2009-01-11 haftmann 2009-01-11 construct explicit class morphism
2009-01-06 haftmann 2009-01-06 locale -> old_locale, new_locale -> locale
2009-01-05 haftmann 2009-01-05 locale -> old_locale, new_locale -> locale
2009-01-05 haftmann 2009-01-05 rearranged target theories