src/Pure/more_thm.ML
24 months ago wenzelm 2017-06-22 consolidate proofs more simultaneously;
2017-04-10 wenzelm 2017-04-10 tuned signature;
2016-12-16 wenzelm 2016-12-16 consolidate nested thms with persistent result, for improved performance; always consolidate parts of fulfill_norm_proof: important to exhibit cyclic thms (via non-termination as officially published), but this was lost in f33d5a00c25d;
2016-12-14 wenzelm 2016-12-14 more careful derivation_closed / close_derivation;
2016-12-13 wenzelm 2016-12-13 more symbols;
2016-06-23 wenzelm 2016-06-23 tuned signature;
2016-04-25 wenzelm 2016-04-25 clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
2016-01-07 wenzelm 2016-01-07 more uniform treatment of package internals;
2015-12-16 wenzelm 2015-12-16 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
2015-12-15 wenzelm 2015-12-15 tuned signature -- clarified modules;
2015-10-23 wenzelm 2015-10-23 print thm wrt. local shyps (from full proof context); tuned;
2015-10-23 wenzelm 2015-10-23 clarified modules; tuned signature;
2015-10-06 wenzelm 2015-10-06 added Thm.forall_intr_name;
2015-10-06 wenzelm 2015-10-06 just one theorem kind, which is legacy anyway;
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-09-25 wenzelm 2015-09-25 tuned;
2015-09-25 wenzelm 2015-09-25 tuned signature: eliminated pointless type Context.pretty;
2015-09-24 wenzelm 2015-09-24 more explicit Defs.context: use proper name spaces as far as possible;
2015-08-30 wenzelm 2015-08-30 trim context for persistent storage;
2015-08-28 wenzelm 2015-08-28 tuned;
2015-08-28 wenzelm 2015-08-28 tuned;
2015-08-28 wenzelm 2015-08-28 tuned signature;
2015-08-16 wenzelm 2015-08-16 produce certified vars without access to theory_of_thm, and without context;
2015-08-16 wenzelm 2015-08-16 produce certified vars without access to theory_of_thm, and without context;
2015-08-16 wenzelm 2015-08-16 tuned;
2015-08-16 wenzelm 2015-08-16 prefer theory_id operations; tuned signature;
2015-08-15 wenzelm 2015-08-15 clarified context;
2015-07-28 wenzelm 2015-07-28 more explicit context; tuned signature;
2015-07-28 wenzelm 2015-07-28 eliminated dead code;
2015-07-28 wenzelm 2015-07-28 more direct access to atomic cterms;
2015-07-28 wenzelm 2015-07-28 proper context;
2015-07-28 wenzelm 2015-07-28 more direct access to atomic cterms;
2015-07-28 wenzelm 2015-07-28 clarified context;
2015-07-27 wenzelm 2015-07-27 tuned signature; clarified context;
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-06-03 wenzelm 2015-06-03 clarified context;
2015-06-01 wenzelm 2015-06-01 tuned;
2015-04-08 wenzelm 2015-04-08 explicitly checked alpha conversion -- actual renaming happens outside kernel;
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-05 wenzelm 2015-03-05 tuned -- more explicit use of context;
2015-03-04 wenzelm 2015-03-04 clarified signature;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-08-18 wenzelm 2014-08-18 more general dummy: may contain "parked arguments", for example;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-02-20 wenzelm 2014-02-20 clarified printing of undeclared hyps;
2014-02-17 wenzelm 2014-02-17 subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
2014-01-11 wenzelm 2014-01-11 check_hyps when attributes are applied;
2014-01-11 wenzelm 2014-01-11 check_hyps for attribute application (still inactive, due to non-compliant tools); bypass check_hyps for locale expressions, where assumptions are not necessarily declared in intermediate situations;
2014-01-10 wenzelm 2014-01-10 more elementary management of declared hyps, below structure Assumption; Goal.prove: insist in declared hyps; Simplifier: declare hyps via Thm.assume_hyps; more accurate tool context in some boundary cases;
2013-08-26 wenzelm 2013-08-26 always transfer thm where attributes are applied -- relevant for internal 'notes' (e.g. via bundle 'includes') in contrast to external 'notes' (cf. Proof_Context.retrieve_thms);
2013-07-17 wenzelm 2013-07-17 more official Thm.eq_thm_strict, without demanding ML equality type;
2013-02-28 wenzelm 2013-02-28 discontinued empty name bindings in 'axiomatization';
2012-09-01 wenzelm 2012-09-01 discontinued complicated/unreliable notion of recent proofs within context;
2012-08-31 wenzelm 2012-08-31 tuned signature;
2012-08-30 wenzelm 2012-08-30 some support for registering forked proofs within Proof.state, using its bottom context; tuned signature;
2012-08-30 wenzelm 2012-08-30 tuned signature;
2012-03-10 wenzelm 2012-03-10 eliminated dead code;