src/Pure/pure_thy.ML
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-08 wenzelm 2010-05-08 renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
2010-04-11 wenzelm 2010-04-11 Thm.add_axiom/add_def: return internal name of foundational axiom;
2010-03-27 wenzelm 2010-03-27 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML); discontinued old-style Theory.add_defs(_i) in favour of more basic Theory.add_def; modernized PureThy.add_defs etc. -- refer to high-level Thm.add_def;
2010-03-22 wenzelm 2010-03-22 replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
2010-03-21 wenzelm 2010-03-21 minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
2010-03-03 wenzelm 2010-03-03 authentic syntax for classes and type constructors; read/intern formal entities just after raw parsing, extern just before final pretty printing; discontinued _class token translation; moved Local_Syntax.extern_term to Syntax/printer.ML; misc tuning;
2010-02-21 wenzelm 2010-02-21 slightly more abstract syntax mark/unmark operations;
2010-02-21 wenzelm 2010-02-21 authentic syntax for *all* term constants;
2010-02-16 wenzelm 2010-02-16 moved generic update_name to Pure syntax -- not specific to HOL/record;
2010-02-15 wenzelm 2010-02-15 renamed InfixName to Infix etc.;
2009-11-15 wenzelm 2009-11-15 eliminated obsolete thm position tags;
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-11-02 wenzelm 2009-11-02 modernized structure Simple_Syntax;
2009-10-30 haftmann 2009-10-30 set Pure theory name properly
2009-10-25 wenzelm 2009-10-25 maintain group via name space, not tags;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-09-30 wenzelm 2009-09-30 eliminated dead code;
2009-07-21 wenzelm 2009-07-21 join_proofs: implicit exception; removed obsolete cancel_proofs, cf. cancel_thy in thy_info.ML; tuned;
2009-07-19 wenzelm 2009-07-19 cancel_proofs: some attempts at reworking group management (based on body promises only);
2009-04-02 wenzelm 2009-04-02 tuned signature;
2009-03-07 wenzelm 2009-03-07 more uniform handling of binding in targets and derived elements;
2009-03-07 wenzelm 2009-03-07 Theory.add_axioms/add_defs: 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 Thm.binding;
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2009-01-10 wenzelm 2009-01-10 added cancel_proofs, based on task groups of "entered" proofs;
2009-01-10 wenzelm 2009-01-10 tuned;
2009-01-10 wenzelm 2009-01-10 simplified join_proofs;
2008-12-23 wenzelm 2008-12-23 renamed terminal category "float" to "float_token", to avoid name space conflicts with actual "float" types in user theories (only "float_const" is encountered in practice anyway); tuned;
2008-12-06 wenzelm 2008-12-06 renamed force_proofs to join_proofs;
2008-12-05 wenzelm 2008-12-05 merged
2008-12-04 wenzelm 2008-12-04 renamed type Lazy.T to lazy; force_proofs: original order;
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-12-01 haftmann 2008-12-01 new Binding module
2008-11-29 nipkow 2008-11-29 New lexical item "float".
2008-11-20 haftmann 2008-11-20 fact table now using name bindings
2008-11-20 haftmann 2008-11-20 using name bindings
2008-11-20 wenzelm 2008-11-20 Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
2008-11-18 wenzelm 2008-11-18 added force_proofs (based on thms ever passed through enter_thms);
2008-10-23 wenzelm 2008-10-23 renamed Thm.get_axiom_i to Thm.axiom;
2008-10-16 wenzelm 2008-10-16 added const sort_constraint with syntax SORT_CONSTRAINT -- logically vacous;
2008-09-02 wenzelm 2008-09-02 name_thm etc.: pass position; note_thms etc.: Name.binding, report fact_decl;
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-08-05 wenzelm 2008-08-05 get_fact: report position;
2008-08-04 wenzelm 2008-08-04 removed obsolete note_thms_cmd;
2008-07-29 haftmann 2008-07-29 PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-07-25 haftmann 2008-07-25 dropped PureThy.note; added PureThy.add_thm
2008-06-14 wenzelm 2008-06-14 removed old theorem database;
2008-05-18 wenzelm 2008-05-18 theory Pure provides regular application syntax by default; added old_appl_syntax_setup for former Pure clients;
2008-04-16 wenzelm 2008-04-16 renamed check_fact to defined_fact;
2008-04-16 wenzelm 2008-04-16 removed obsolete get_fact_silent; PureThy.get_fact: pass dynamic context; tuned;
2008-04-15 wenzelm 2008-04-15 added intern_fact, check_fact, hide_fact; renamed all_facts_of to facts_of; removed hide_thms; Sign.hide_const;
2008-04-15 wenzelm 2008-04-15 moved forall_elim_var(s) to more_thm.ML; get_thm(s) and hide_thms: use new table;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-03 wenzelm 2008-04-03 removed obsolete add_axiomss(_i);
2008-03-29 wenzelm 2008-03-29 eliminated destructive/critical theorem database; simplified store_thm(s); removed obsolete smart_store_thm(s); tuned;
2008-03-28 wenzelm 2008-03-28 NAMED_CRITICAL;