src/Pure/Isar/element.ML
2012-04-27 wenzelm 2012-04-27 clarified signature;
2012-04-01 wenzelm 2012-04-01 added Attrib.global_notes/local_notes/generic_notes convenience;
2012-03-13 wenzelm 2012-03-13 refined 'interpret': reset facts ("this") and print_result, which merely consist of internal / protected statement;
2012-03-13 wenzelm 2012-03-13 tuned;
2012-03-10 wenzelm 2012-03-10 tuned;
2012-02-28 wenzelm 2012-02-28 display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
2011-11-20 wenzelm 2011-11-20 tuned signature;
2011-11-19 wenzelm 2011-11-19 do not store vacuous theorem specifications -- relevant for frugal local theory content; tuned;
2011-11-07 wenzelm 2011-11-07 tuned signature -- avoid spurious Thm.mixed_attribute;
2011-11-05 wenzelm 2011-11-05 more uniform instT_subst vs. inst_subst: compare variable names only;
2011-11-05 wenzelm 2011-11-05 some performance tuning via Term_Subst/Same.operation; tuned;
2011-11-05 wenzelm 2011-11-05 pruned signature;
2011-11-03 wenzelm 2011-11-03 tuned whitespace;
2011-10-29 wenzelm 2011-10-29 tuned;
2011-10-28 wenzelm 2011-10-28 tuned signature -- refined terminology;
2011-10-28 wenzelm 2011-10-28 slightly more explicit/syntactic modelling of morphisms;
2011-08-08 wenzelm 2011-08-08 misc tuning -- eliminated old-fashioned rep_thm;
2011-07-15 wenzelm 2011-07-15 Element.activate: leave check of binding where actually applied to the context -- allow internal qualifications, or non-identifier fact names like "assumes *: A" (see also 1183951365de);
2011-07-15 wenzelm 2011-07-15 do not check vacous bindings, which routinely occur in locale expressions and long theorem statements etc.;
2011-06-25 wenzelm 2011-06-25 clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
2011-04-27 wenzelm 2011-04-27 clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
2011-04-27 wenzelm 2011-04-27 tuned signature -- eliminated odd comment;
2011-04-27 wenzelm 2011-04-27 reorganized fixes as specialized (global) name space;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 tuned signature, disentangled dependencies;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;
2011-01-15 wenzelm 2011-01-15 clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
2011-01-03 haftmann 2011-01-03 tuned whitespace
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-06 wenzelm 2010-09-06 turned show_hyps and show_tags into proper configuration option;
2010-08-25 wenzelm 2010-08-25 structure Thm: less pervasive names;
2010-07-31 ballarin 2010-07-31 Interpretation in proofs supports mixins.
2010-05-05 haftmann 2010-05-05 eq_morphism is always optional: avoid trivial morphism for empty list of equations
2010-04-25 wenzelm 2010-04-25 modernized naming conventions of main Isar proof elements;
2010-03-13 wenzelm 2010-03-13 removed unused Args.maxidx_values and Element.generalize_facts;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Display;
2009-07-26 wenzelm 2009-07-26 Variable.focus: named parameters;
2009-07-25 wenzelm 2009-07-25 Method.Basic: no position;
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-06-24 wenzelm 2009-06-24 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported); renamed Variable.importT_thms to Variable.importT (again);
2009-03-29 wenzelm 2009-03-29 simplified Element.activate(_i): singleton version;
2009-03-29 wenzelm 2009-03-29 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML; tuned;
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-19 wenzelm 2009-03-19 use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-11 wenzelm 2009-03-11 eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
2009-03-11 wenzelm 2009-03-11 Thm.def_binding_optional;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
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-03-03 wenzelm 2009-03-03 Binding.str_of; pretty_name_atts: check Binding.is_empty, not result of Binding.str_of;
2009-03-03 wenzelm 2009-03-03 Thm.binding;
2009-01-21 wenzelm 2009-01-21 eliminated obsolete var morphism; simplified map_ctxt: just one version, without var; removed obsolete params_of, prems_of, facts_of; removed obsolete rename operations; tuned;
2009-01-21 haftmann 2009-01-21 refined witness algebra