src/Pure/Isar/element.ML
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
2009-01-17 haftmann 2009-01-17 explicit equation morphism
2008-12-16 ballarin 2008-12-16 Transfer morphism with theory closure.
2008-12-16 ballarin 2008-12-16 Finer-grained activation so that facts from earlier elements are available.
2008-12-16 ballarin 2008-12-16 Use correct mode when parsing elements and conclusion.
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-25 ballarin 2008-11-25 Use standard export function.
2008-11-20 haftmann 2008-11-20 tuned name bindings
2008-11-19 ballarin 2008-11-19 Basic types not qualified.
2008-11-18 ballarin 2008-11-18 Activate elements moved to element.ML.
2008-11-13 haftmann 2008-11-13 diagnostic output for name bindings
2008-11-10 haftmann 2008-11-10 more verbose element printing
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; name/var morphism operates on Name.binding;
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-04-18 wenzelm 2008-04-18 tuned;
2008-04-17 wenzelm 2008-04-17 print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);
2008-04-12 wenzelm 2008-04-12 replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2007-12-21 ballarin 2007-12-21 Fixed eta constraction issue in compose_witness
2007-12-14 wenzelm 2007-12-14 added close_witness;
2007-11-05 wenzelm 2007-11-05 tuned satisfy_thm;
2007-11-05 ballarin 2007-11-05 Removed inst_morphism'; satisfy_thm avoids compose.
2007-10-26 wenzelm 2007-10-26 proven witness: proper Goal.close_result save huge amounts of resources when using proof terms;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-09-18 ballarin 2007-09-18 New function inst_morphism'.
2007-08-03 wenzelm 2007-08-03 replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
2007-06-18 wenzelm 2007-06-18 tuned conjunction tactics: slightly smaller proof terms;
2007-06-13 wenzelm 2007-06-13 Method.Basic: include position;
2007-05-10 wenzelm 2007-05-10 moved conversions to structure Conv;
2007-04-15 wenzelm 2007-04-15 Thm.fold_terms;
2007-04-14 wenzelm 2007-04-14 inst(T)_morphism: avoid reference to static theory value;
2007-04-13 ballarin 2007-04-13 Experimental interpretation code for definitions.
2007-04-03 wenzelm 2007-04-03 renamed Variable.import to import_thms (avoid clash with Alice keywords);
2006-12-30 wenzelm 2006-12-30 pretty_statement: more careful handling of name_hint;
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;