src/Pure/Isar/isar_cmd.ML
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;
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 report doc_source;
2008-08-14 wenzelm 2008-08-14 oracle, header/local_theory/proof_markup: pass SymbolPos.text;
2008-08-13 wenzelm 2008-08-13 simplified markup commands -- removed obsolete Present.results, always check text;
2008-08-04 wenzelm 2008-08-04 removed obsolete apply_theorems(_i);
2008-07-29 haftmann 2008-07-29 PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-07-15 wenzelm 2008-07-15 renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
2008-07-14 haftmann 2008-07-14 dropped junk
2008-07-14 wenzelm 2008-07-14 renamed theory to init_theory, removed obsolete kill argument; removed unused init_toplevel, begin_theory, end_theory; print_theorems: Toplevel.previous_node_of;
2008-07-14 wenzelm 2008-07-14 removed obsolete history commands; moved back, cannot_undo to isar_syn.ML;
2008-07-08 wenzelm 2008-07-08 moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy; removed unused touch_child_thys, touch_thy, remove_thy, kill_thy;
2008-07-02 wenzelm 2008-07-02 Toplevel.init_theory: pass name explicitly;
2008-06-25 wenzelm 2008-06-25 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces; moved check_text here;
2008-06-18 wenzelm 2008-06-18 moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
2008-06-14 wenzelm 2008-06-14 removed exotic 'token_translation' command;
2008-04-17 wenzelm 2008-04-17 token translations: context dependent, result Pretty.T; string_of_term/prop: Variable.auto_fixes;
2008-04-16 wenzelm 2008-04-16 PureThy.defined_fact; unused_thms: simplified signature;
2008-04-15 wenzelm 2008-04-15 added hide_names command (formerly Sign.hide_names), support fact name space;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-10 wenzelm 2008-04-10 Context.set_thread_data: non-critical;
2008-03-29 wenzelm 2008-03-29 simplified print_simpset;
2008-03-29 wenzelm 2008-03-29 removed obsolete use_XXX; added ml_diag;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-28 wenzelm 2008-03-28 reorganized signature of ML_Context;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-27 wenzelm 2008-03-27 renamed ML_Context.the_context to ML_Context.the_global_context;
2008-03-26 wenzelm 2008-03-26 adapted to Context.thread_data interface;
2008-03-26 wenzelm 2008-03-26 removed obsolete use_thy (cf. isar_syn.ML);
2008-03-24 wenzelm 2008-03-24 ML runtime compilation: pass position, tuned signature;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-02-28 wenzelm 2008-02-28 unused_thms: print via official context (ProofContext.pretty_fact), not just the theory certificate (Display.pretty_thm); tuned;
2008-02-28 berghofe 2008-02-28 Added unused_thms command.
2008-02-15 wenzelm 2008-02-15 tuned names;
2008-02-10 wenzelm 2008-02-10 tuned default position;
2008-01-24 wenzelm 2008-01-24 removed unused Toplevel.properties;
2008-01-03 wenzelm 2008-01-03 nested_command: simplified properties vs. position -- the latter also includes id now;
2008-01-02 wenzelm 2008-01-02 added nested_command (with explicit position argument via properties);