src/Pure/Isar/isar_syn.ML
2010-04-28 ago localized default sort;
2010-04-28 ago modernized/simplified Sign.set_defsort;
2010-04-26 ago command 'example_proof' opens an empty proof body;
2010-04-25 ago modernized naming conventions of main Isar proof elements;
2010-04-23 ago explicit 'schematic_theorem' etc. for schematic theorem statements;
2010-04-16 ago keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
2010-04-16 ago replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-04-16 ago modernized old-style type abbreviations;
2010-04-16 ago local type abbreviations;
2010-04-11 ago user interface for abstract datatypes is an attribute, not a command
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.