2009-11-13 ago modernized structure Local_Theory;
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 structure Thm_Deps;
2009-11-02 ago modernized structure Proof_Display;
2009-11-02 ago modernized structure Proof_Syntax;
2009-11-01 ago modernized structure Context_Rules;
2009-10-28 ago renamed Proof.flat_goal to Proof.simple_goal;
2009-10-27 ago ProofContext.setmp_verbose_CRITICAL;
2009-10-24 ago renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-02 ago replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
2009-09-29 ago Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
2009-07-23 ago renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-19 ago parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
2009-06-27 ago tune File.isabelle_tool signature;
2009-03-30 ago tuned;
2009-03-30 ago added Toplevel.previous_node_of;
2009-03-18 ago more precise type Symbol_Pos.text;
2009-03-18 ago de-camelized Symbol_Pos;
2009-03-15 ago ML_Syntax.make_binding;
2009-03-11 ago added 'local_setup' command;
2009-03-08 ago simplified presentation: pass state directly;
2009-03-08 ago proper context for Simplifier.pretty_ss;
2009-03-07 ago Theory.add_axioms/add_defs: replaced old bstring by binding;
2009-03-07 ago oracle: proper name position, tuned;
2009-03-05 ago Thm.add_oracle interface: replaced old bstring by binding;
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-03 ago renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
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 binding replaces bstring
2009-01-07 ago qed/after_qed: singleton result;
2009-01-05 ago locale -> old_locale, new_locale -> locale
2008-12-12 ago Merged.
2008-12-11 ago Conversion of HOL-Main and ZF to new locales.
2008-12-11 ago print_theorems: more robust difference, even after finished proof;
2008-12-05 ago Name.name_of -> Binding.base_name
2008-12-04 ago cleaned up binding module and related code
2008-11-16 ago clarified Thm.proof_body_of vs. Thm.proof_of;
2008-11-15 ago Thm.proof_of returns proof_body;
2008-10-04 ago renamed isatool to isabelle_tool in programming interfaces;
2008-09-26 ago eliminated polymorphic equality;
2008-09-18 ago simplified oracle interface;
2008-09-17 ago simplified ML_Context.eval_in -- expect immutable Proof.context value;
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 report doc_source;
2008-08-14 ago oracle, header/local_theory/proof_markup: pass SymbolPos.text;
2008-08-13 ago simplified markup commands -- removed obsolete Present.results, always check text;
2008-08-04 ago removed obsolete apply_theorems(_i);
2008-07-29 ago PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-07-15 ago renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
2008-07-14 ago dropped junk
2008-07-14 ago renamed theory to init_theory, removed obsolete kill argument;
2008-07-14 ago removed obsolete history commands;
2008-07-08 ago moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;