src/Pure/Isar/isar_syn.ML
2008-12-11 ballarin 2008-12-11 Conversion of HOL-Main and ZF to new locales.
2008-12-10 ballarin 2008-12-10 Enable keyword 'structure' in for clause of locale expression.
2008-12-05 haftmann 2008-12-05 Name.name_of -> Binding.base_name
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-12-03 ballarin 2008-12-03 Sublocale: removed public after_qed; identifiers private to NewLocale.
2008-11-28 ballarin 2008-11-28 Ahere to modern naming conventions; proper treatment of internal vs external names.
2008-11-27 ballarin 2008-11-27 Sublocale command.
2008-11-17 haftmann 2008-11-17 adjusted locale signature to *_cmd convention
2008-11-06 ballarin 2008-11-06 Keyword 'includes' gone.
2008-09-19 wenzelm 2008-09-19 moved Isar editor commands from isar_syn.ML to isar.ML; P.props_text;
2008-09-18 wenzelm 2008-09-18 simplified oracle interface;
2008-09-17 wenzelm 2008-09-17 ML_prf: inherit env for all contexts within the proof;
2008-09-17 wenzelm 2008-09-17 added ML_prf;
2008-09-17 ballarin 2008-09-17 Public interface to interpretation morphism.
2008-09-03 wenzelm 2008-09-03 axiomatization is now global-only;
2008-09-02 ballarin 2008-09-02 Interpretation commands no longer accept interpretation attributes.
2008-09-02 wenzelm 2008-09-02 type Attrib.binding abbreviates Name.binding without attributes; Attrib.no_binding refers to Name.no_binding;
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-08-14 wenzelm 2008-08-14 renamed P.ml_source to P.ML_source;
2008-08-14 wenzelm 2008-08-14 P.doc_source and P.ml_sorce for proper SymbolPos.text;
2008-08-13 wenzelm 2008-08-13 simplified markup commands;
2008-08-12 wenzelm 2008-08-12 Isabelle.command: inline former OuterSyntax.prepare_command; Isar.command: based on fail-safe OuterSyntax.prepare_command;
2008-08-11 wenzelm 2008-08-11 Isar.command: OuterSyntax.prepare_command_failsafe defers syntax errors until execution time;
2008-08-11 wenzelm 2008-08-11 Isar.command: do not set position of enclosing transaction, to avoid of clash with the one being prepared here!
2008-08-04 wenzelm 2008-08-04 Isar.command: explicitly set transaction position, as required for prepare_command errors; adapted Isabelle.command;
2008-07-25 haftmann 2008-07-25 dropped locale (open)
2008-07-16 wenzelm 2008-07-16 added Isar.command, Isar.insert, Isar.remove (editor model);
2008-07-15 wenzelm 2008-07-15 renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
2008-07-14 wenzelm 2008-07-14 adapted IsarCmd.init_theory;
2008-07-14 wenzelm 2008-07-14 removed obsolete 'redo' command; cannot_undo: global history; tuned;
2008-07-10 wenzelm 2008-07-10 activated new versions of init_toplevel, linear_undo, undo, undos_proof kill;
2008-07-10 wenzelm 2008-07-10 added Isar.init_point, Isar.kill;
2008-07-10 wenzelm 2008-07-10 added Isar.linear_undo;
2008-07-10 wenzelm 2008-07-10 added Isar.undo, which emulates old-style undo on global tty state;
2008-07-08 wenzelm 2008-07-08 removed obsolete touch_child_thys; simplified touch_thy, remove_thy, kill_thy -- inlined;
2008-06-28 wenzelm 2008-06-28 tuned;
2008-06-25 wenzelm 2008-06-25 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-14 wenzelm 2008-06-14 removed exotic 'token_translation' command;
2008-06-10 haftmann 2008-06-10 dropped instance with attached definitions
2008-05-24 wenzelm 2008-05-24 more uniform treatment of OuterSyntax.local_theory commands;
2008-05-14 wenzelm 2008-05-14 remobed obsolete keyword concl;
2008-04-15 wenzelm 2008-04-15 proof endings: no Toplevel.print!
2008-04-15 wenzelm 2008-04-15 IsarCmd.hide_names;
2008-04-10 wenzelm 2008-04-10 eliminated unused Toplevel.print3/three_buffers;
2008-04-02 haftmann 2008-04-02 removed obscure "attach" feature
2008-03-29 wenzelm 2008-03-29 commands 'use' and 'ML' now thy_decl; removed obsolete 'ML_setup' -- superceded by 'ML';
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-26 wenzelm 2008-03-26 use_thy: removed obsolete ML_Context.save;
2008-03-25 wenzelm 2008-03-25 added 'ML_val' command (diagnostic);
2008-03-24 wenzelm 2008-03-24 ML runtime compilation: pass position, tuned signature;
2008-03-10 haftmann 2008-03-10 dropped "include" feature of classes
2008-02-28 berghofe 2008-02-28 Added unused_thms command.
2008-02-09 wenzelm 2008-02-09 overloading: tuned signature;
2008-01-08 haftmann 2008-01-08 refined overloading target
2008-01-02 wenzelm 2008-01-02 Isabelle.command: IsarCmd.nested_command (with properties);
2007-12-14 wenzelm 2007-12-14 nested commands: avoid nested errors;
2007-12-08 wenzelm 2007-12-08 tuned message;
2007-12-08 wenzelm 2007-12-08 tuned messages;
2007-12-07 wenzelm 2007-12-07 added nested 'Isabelle.command';
2007-12-05 haftmann 2007-12-05 improved