src/Pure/Isar/isar_syn.ML
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;
2008-09-17 ago ML_prf: inherit env for all contexts within the proof;
2008-09-17 ago added ML_prf;
2008-09-17 ago Public interface to interpretation morphism.
2008-09-03 ago axiomatization is now global-only;
2008-09-02 ago Interpretation commands no longer accept interpretation attributes.
2008-09-02 ago type Attrib.binding abbreviates Name.binding without attributes;
2008-09-02 ago explicit type Name.binding for higher-specification elements;
2008-08-14 ago renamed P.ml_source to P.ML_source;
2008-08-14 ago P.doc_source and P.ml_sorce for proper SymbolPos.text;
2008-08-13 ago simplified markup commands;
2008-08-12 ago Isabelle.command: inline former OuterSyntax.prepare_command;
2008-08-11 ago Isar.command: OuterSyntax.prepare_command_failsafe defers syntax errors until execution time;
2008-08-11 ago Isar.command: do not set position of enclosing transaction, to avoid of clash with the one being prepared here!
2008-08-04 ago Isar.command: explicitly set transaction position, as required for prepare_command errors;
2008-07-25 ago dropped locale (open)
2008-07-16 ago added Isar.command, Isar.insert, Isar.remove (editor model);
2008-07-15 ago renamed IsarCmd.nested_command to OuterSyntax.prepare_command;