src/Pure/Isar/isar_syn.ML
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-01 wenzelm 2010-03-01 added type_notation command;
2010-02-24 wenzelm 2010-02-24 allow general mixfix syntax for type constructors;
2010-02-23 haftmann 2010-02-23 dropped axclass
2010-02-19 haftmann 2010-02-19 added code_abstype keyword
2010-02-18 wenzelm 2010-02-18 removed unused Theory_Target.begin; Theory_Target.init: removed Locale.intern, which was accidentally introduced in 40b3630b0deb; renamed Theory_Target.context to Theory_Target.context_cmd to emphasize that this involves Locale.intern; tuned;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-10 wenzelm 2009-11-10 modernized structure Theory_Target;
2009-11-08 wenzelm 2009-11-08 print_theorems: suppress concealed (global) facts, unless "!" option is given;
2009-11-05 wenzelm 2009-11-05 allow "pervasive" local theory declarations, which are applied the background theory;
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Node;
2009-10-28 wenzelm 2009-10-28 provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
2009-10-01 ballarin 2009-10-01 Merged.
2009-09-29 ballarin 2009-09-29 Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
2009-09-01 wenzelm 2009-09-01 modernized Thy_Header;
2009-06-29 haftmann 2009-06-29 mutual instances
2009-06-01 wenzelm 2009-06-01 ML_Env;
2009-05-12 haftmann 2009-05-12 transferred code generator preprocessor into separate module
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes within locale expression are mandatory by default;
2009-03-24 wenzelm 2009-03-24 tuned;
2009-03-19 wenzelm 2009-03-19 command 'use', 'ML': apply ML environment to theory and target as well; tuned command descriptions;
2009-03-18 wenzelm 2009-03-18 generalized ML_Context.inherit_env;
2009-03-16 wenzelm 2009-03-16 adapted 'method_setup' command to Method.setup;
2009-03-15 wenzelm 2009-03-15 added 'attribute_setup' command;
2009-03-12 wenzelm 2009-03-12 old name_spec for 'axioms' and 'defs' (from spec_parse.ML);
2009-03-11 wenzelm 2009-03-11 added 'local_setup' command; tuned;
2009-03-07 wenzelm 2009-03-07 more uniform handling of binding in targets and derived elements;
2009-03-07 wenzelm 2009-03-07 oracle: proper name position, tuned;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
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;