src/Pure/Isar/isar_syn.ML
2009-03-01 wenzelm 2009-03-01 discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
2009-02-28 wenzelm 2009-02-28 moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
2009-02-27 wenzelm 2009-02-27 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
2009-02-13 kleing 2009-02-13 New command find_consts searching for constants by type (by Timothy Bourke).
2009-02-11 kleing 2009-02-11 FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
2009-01-21 haftmann 2009-01-21 allow empty class specs
2009-01-21 haftmann 2009-01-21 wrecked old locale package and related modules
2009-01-07 haftmann 2009-01-07 changed locale predicate name convention
2009-01-07 haftmann 2009-01-07 proper local_theory after Class.class
2009-01-06 haftmann 2009-01-06 merged
2009-01-05 haftmann 2009-01-05 locale -> old_locale, new_locale -> locale
2009-01-05 haftmann 2009-01-05 rearranged target theories
2009-01-05 wenzelm 2009-01-05 Isar.init;
2009-01-02 wenzelm 2009-01-02 added props_text (from outer_parse.ML);
2008-12-12 ballarin 2008-12-12 Merged; updated interpretation command in 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