2010-03-21 ago minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
2010-03-18 ago typedecl: no sort constraints;
2010-03-09 ago localized typedecl;
2010-03-07 ago separate structure Typedecl;
2010-03-07 ago modernized structure Object_Logic;
2010-03-01 ago added type_notation command;
2010-02-24 ago allow general mixfix syntax for type constructors;
2010-02-23 ago dropped axclass
2010-02-19 ago added code_abstype keyword
2010-02-18 ago removed unused Theory_Target.begin;
2009-11-13 ago modernized structure Local_Theory;
2009-11-10 ago modernized structure Theory_Target;
2009-11-08 ago print_theorems: suppress concealed (global) facts, unless "!" option is given;
2009-11-05 ago allow "pervasive" local theory declarations, which are applied the background theory;
2009-11-02 ago modernized structure Proof_Node;
2009-10-28 ago provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
2009-10-01 ago Merged.
2009-09-29 ago Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
2009-09-01 ago modernized Thy_Header;
2009-06-29 ago mutual instances
2009-06-01 ago ML_Env;
2009-05-12 ago transferred code generator preprocessor into separate module
2009-03-26 ago interpretation/interpret: prefixes within locale expression are mandatory by default;
2009-03-24 ago tuned;
2009-03-19 ago command 'use', 'ML': apply ML environment to theory and target as well;
2009-03-18 ago generalized ML_Context.inherit_env;
2009-03-16 ago adapted 'method_setup' command to Method.setup;
2009-03-15 ago added 'attribute_setup' command;
2009-03-12 ago old name_spec for 'axioms' and 'defs' (from spec_parse.ML);
2009-03-11 ago added 'local_setup' command;
2009-03-07 ago more uniform handling of binding in targets and derived elements;
2009-03-07 ago oracle: proper name position, tuned;
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-01 ago discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
2009-02-28 ago moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
2009-02-27 ago moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
2009-02-13 ago New command find_consts searching for constants by type (by Timothy Bourke).
2009-02-11 ago FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
2009-01-21 ago allow empty class specs
2009-01-21 ago wrecked old locale package and related modules
2009-01-07 ago changed locale predicate name convention
2009-01-07 ago proper local_theory after Class.class
2009-01-06 ago merged
2009-01-05 ago locale -> old_locale, new_locale -> locale
2009-01-05 ago rearranged target theories
2009-01-05 ago Isar.init;
2009-01-02 ago added props_text (from outer_parse.ML);
2008-12-12 ago Merged; updated interpretation command in isar_syn.ML.
2008-12-11 ago Conversion of HOL-Main and ZF to new locales.
2008-12-10 ago Enable keyword 'structure' in for clause of locale expression.
2008-12-05 ago Name.name_of -> Binding.base_name
2008-12-04 ago cleaned up binding module and related code
2008-12-03 ago Sublocale: removed public after_qed; identifiers private to NewLocale.
2008-11-28 ago Ahere to modern naming conventions; proper treatment of internal vs external names.
2008-11-27 ago Sublocale command.
2008-11-17 ago adjusted locale signature to *_cmd convention
2008-11-06 ago Keyword 'includes' gone.
2008-09-19 ago moved Isar editor commands from isar_syn.ML to isar.ML;
2008-09-18 ago simplified oracle interface;