src/Pure/axclass.ML
2016-05-09 wenzelm 2016-05-09 clarified context, notably for internal use of Simplifier;
2016-04-07 wenzelm 2016-04-07 prefer regular context update, to allow continuous editing of Pure;
2015-09-25 wenzelm 2015-09-25 tuned signature: eliminated pointless type Context.pretty;
2015-09-22 wenzelm 2015-09-22 tuned signature;
2015-09-22 wenzelm 2015-09-22 eliminated separate type Theory.dep: use typeargs uniformly for consts/types; Object_Logic.add_judgment more like Theory.specify_const;
2015-09-22 wenzelm 2015-09-22 tuned whitespace;
2015-09-22 wenzelm 2015-09-22 HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015; defs.ML: track dependencies also for type constructors; typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type; Pure types and typedecls are final -- no dependencies;
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-03-31 wenzelm 2015-03-31 tuned signature;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-23 wenzelm 2015-02-23 Goal.prove_multi is superseded by the fully general Goal.prove_common;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-05-12 wenzelm 2014-05-12 tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";
2014-03-14 wenzelm 2014-03-14 conceal somewhat obscure internal facts, e.g. relevant for 'print_theorems', 'find_theorems';
2014-02-10 wenzelm 2014-02-10 discontinued axiomatic 'classes', 'classrel', 'arities';
2014-01-06 haftmann 2014-01-06 uniform orientation of instances as (type constructor, type class)
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-08-23 wenzelm 2013-08-23 added Theory.setup convenience;
2013-07-30 wenzelm 2013-07-30 type theory is purely value-oriented;
2013-05-30 wenzelm 2013-05-30 standardized aliases;
2013-04-10 wenzelm 2013-04-10 more standard module name Axclass (according to file name);
2013-04-10 wenzelm 2013-04-10 formal proof context for axclass proofs; avoid global_simpset_of -- refer to simpset of proof context;
2013-01-08 wenzelm 2013-01-08 tuned;
2013-01-08 wenzelm 2013-01-08 tuned -- prefer high-level Table.merge with its slightly more conservative update;
2013-01-07 wenzelm 2013-01-07 more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed; transfer theorems where they are picked from the theory; tuned;
2013-01-07 wenzelm 2013-01-07 tuned comment -- do not claim anything;
2011-08-20 wenzelm 2011-08-20 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
2011-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2011-04-18 wenzelm 2011-04-18 pass plain Proof.context for pretty printing;
2011-04-18 wenzelm 2011-04-18 simplified pretty printing context, which is only required for certain kernel operations; disentangled dependencies of structure Pretty;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
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-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-09-05 wenzelm 2010-09-05 pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
2010-08-11 haftmann 2010-08-11 tuned whitespace
2010-06-01 haftmann 2010-06-01 avoid store flag in add_* operations
2010-06-01 haftmann 2010-06-01 do not expose store flag of AxClass.add_*
2010-06-01 berghofe 2010-06-01 classrel and arity theorems are now stored under proper name in theory. add_arity and add_classrel take extra boolean argument indicating whether theorems should be stored.
2010-05-15 wenzelm 2010-05-15 eliminated redundant runtime checks;
2010-05-15 krauss 2010-05-15 normalize atyp names after unconstrainT, which may rename atyps arbitrarily;
2010-05-13 wenzelm 2010-05-13 the_classrel/the_arity: avoid Thm.transfer for proofterm version -- theory might already have become stale within the proof_body future;
2010-05-09 wenzelm 2010-05-09 just one version of Thm.unconstrainT, which affects all variables; temporary workaround for Nbe.lift_triv_classes_conv;
2010-05-08 wenzelm 2010-05-08 back-patching of axclass proofs;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-28 wenzelm 2010-04-28 made SML/NJ happy;
2010-04-27 wenzelm 2010-04-27 removed obsolete sanity check -- Sign.certify_sort is stable;
2010-04-27 wenzelm 2010-04-27 tuned signature;
2010-04-27 wenzelm 2010-04-27 tuned classrel completion -- bypass composition with reflexive edges;
2010-04-27 wenzelm 2010-04-27 tuned diff_classrels -- avoid slightly inefficient Symreltab.keys;
2010-04-27 wenzelm 2010-04-27 tuned aritiy completion -- slightly less intermediate data structures;
2010-04-27 wenzelm 2010-04-27 clarified proven results: store thm only and retrieve proof later via Thm.proof_of (this may also impact parallelism, because internal join_proofs is deferred);
2010-04-27 wenzelm 2010-04-27 misc tuning and simplification;
2010-04-26 wenzelm 2010-04-26 removed unused AxClass.class_intros;
2010-04-25 wenzelm 2010-04-25 renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp; less pervasive names;
2010-04-25 wenzelm 2010-04-25 more systematic treatment of data -- avoid slightly odd nested tuples here; tuned;
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 misc tuning and simplification;