2010-05-30 wenzelm 2010-05-30 replaced ML_Lex.read_antiq by more concise, which includes full read/report with explicit position information; ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information; fall back on ML_Context.eval_text if there is no position or no surrounding text; proper Args.name_source_position for method "tactic" and "raw_tactic"; tuned;
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2010-05-08 wenzelm 2010-05-08 unified/simplified Pretty.margin_default; discontinued special Pretty.setmargin etc; explicit margin argument for Pretty.string_of_margin etc.;
2010-04-25 wenzelm 2010-04-25 replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
2010-04-25 wenzelm 2010-04-25 modernized naming conventions of main Isar proof elements;
2010-04-16 wenzelm 2010-04-16 keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-04-16 wenzelm 2010-04-16 modernized old-style type abbreviations;
2010-03-22 wenzelm 2010-03-22 added Specification.axiom convenience;
2010-03-21 wenzelm 2010-03-21 minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
2010-02-16 wenzelm 2010-02-16 simplified meaning of ProofContext.verbose; eliminated strange ProofContext.setmp_verbose_CRITICAL; less confusing printing of (cumulative) unnamed facts;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
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 structure Thm_Deps;
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Display;
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Syntax;
2009-11-01 wenzelm 2009-11-01 modernized structure Context_Rules;
2009-10-28 wenzelm 2009-10-28 renamed Proof.flat_goal to Proof.simple_goal;
2009-10-27 wenzelm 2009-10-27 ProofContext.setmp_verbose_CRITICAL;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-02 wenzelm 2009-10-02 replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
2009-09-29 ballarin 2009-09-29 Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-19 wenzelm 2009-07-19 parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
2009-06-27 wenzelm 2009-06-27 tune File.isabelle_tool signature;
2009-03-30 wenzelm 2009-03-30 tuned;
2009-03-30 wenzelm 2009-03-30 added Toplevel.previous_node_of; keep type Toplevel.node private (formerly required in document antiquotations, which now operate on plain Toplevel.state);
2009-03-18 wenzelm 2009-03-18 more precise type Symbol_Pos.text;
2009-03-18 wenzelm 2009-03-18 de-camelized Symbol_Pos;
2009-03-15 wenzelm 2009-03-15 ML_Syntax.make_binding;
2009-03-11 wenzelm 2009-03-11 added 'local_setup' command; tuned;
2009-03-08 wenzelm 2009-03-08 simplified presentation: pass state directly;
2009-03-08 wenzelm 2009-03-08 proper context for Simplifier.pretty_ss;
2009-03-07 wenzelm 2009-03-07 Theory.add_axioms/add_defs: replaced old bstring by binding;
2009-03-07 wenzelm 2009-03-07 oracle: proper name position, tuned;
2009-03-05 wenzelm 2009-03-05 Thm.add_oracle interface: replaced old bstring by binding;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-03 wenzelm 2009-03-03 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; minor tuning;
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 binding replaces bstring
2009-01-07 wenzelm 2009-01-07 qed/after_qed: singleton result;
2009-01-05 haftmann 2009-01-05 locale -> old_locale, new_locale -> locale
2008-12-12 ballarin 2008-12-12 Merged.
2008-12-11 ballarin 2008-12-11 Conversion of HOL-Main and ZF to new locales.
2008-12-11 wenzelm 2008-12-11 print_theorems: more robust difference, even after finished proof;
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-11-16 wenzelm 2008-11-16 clarified Thm.proof_body_of vs. Thm.proof_of;
2008-11-15 wenzelm 2008-11-15 Thm.proof_of returns proof_body;
2008-10-04 wenzelm 2008-10-04 renamed isatool to isabelle_tool in programming interfaces;
2008-09-26 wenzelm 2008-09-26 eliminated polymorphic equality;
2008-09-18 wenzelm 2008-09-18 simplified oracle interface;
2008-09-17 wenzelm 2008-09-17 simplified ML_Context.eval_in -- expect immutable Proof.context value;