src/Pure/drule.ML
9 months ago wenzelm 2019-08-09 formal position for PThm nodes;
9 months ago wenzelm 2019-08-06 more robust and convenient treatment of implicit context;
10 months ago wenzelm 2019-08-02 clarified modules: inference kernel maintains sort algebra within the logic;
13 months ago wenzelm 2019-04-13 meson: more cterm operations;
13 months ago wenzelm 2019-04-13 tuned signature -- more ctyp operations;
20 months ago wenzelm 2018-10-01 tuned;
20 months ago wenzelm 2018-09-20 clarified standardization of variables, with proper treatment of local variables; tuned signature; tuned;
22 months ago wenzelm 2018-08-06 export shyps as regular typargs;
23 months ago wenzelm 2018-06-29 disallow hyps in export; handle extra shyps as explicit sort constraints;
2018-02-25 wenzelm 2018-02-25 eliminated ASCII syntax from Pure bootstrap; tuned comments;
2016-12-13 wenzelm 2016-12-13 more symbols;
2016-04-28 wenzelm 2016-04-28 unfold is subject to unfold_abs_def (still inactive); tuned signature;
2016-04-05 wenzelm 2016-04-05 clarified modules -- simplified bootstrap;
2015-12-15 wenzelm 2015-12-15 tuned signature -- clarified modules;
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 added Thm.chyps_of; eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf);
2015-07-28 wenzelm 2015-07-28 more explicit context; tuned signature;
2015-07-28 wenzelm 2015-07-28 clarified Variable.gen_all; simplified Local_Defs.export: pointless partial application;
2015-07-28 wenzelm 2015-07-28 more explicit context;
2015-07-28 wenzelm 2015-07-28 more direct access to atomic cterms;
2015-07-27 wenzelm 2015-07-27 tuned signature; clarified context;
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-07-27 wenzelm 2015-07-27 more explicit checks -- improved errors;
2015-07-27 wenzelm 2015-07-27 eliminated cterm_instantiate;
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-07-27 wenzelm 2015-07-27 added infer_instantiate_vars, which allows inconsistent types for variables, as required for Metis proof reconstruction;
2015-07-26 wenzelm 2015-07-26 ignore non-existant variables, like other instantiate rules;
2015-07-26 wenzelm 2015-07-26 added infer_instantiate'; clarified boundary cases of instantiate';
2015-07-26 wenzelm 2015-07-26 more uniform exceptions, like cterm_instantiate;
2015-07-25 wenzelm 2015-07-25 more accurate maxidx;
2015-07-25 wenzelm 2015-07-25 clarified error;
2015-07-25 wenzelm 2015-07-25 added infer_instantiate, which is meant to supersede cterm_instantiate;
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-05-31 wenzelm 2015-05-31 obsolete;
2015-05-31 wenzelm 2015-05-31 tuned;
2015-05-30 wenzelm 2015-05-30 standardize towards Thm.eta_long_conversion, which just does eta_long conversion;
2015-05-30 wenzelm 2015-05-30 tuned;
2015-05-30 wenzelm 2015-05-30 more explicit context;
2015-05-30 wenzelm 2015-05-30 obsolete;
2015-05-30 wenzelm 2015-05-30 tuned -- more direct Thm.renamed_prop;
2015-05-03 wenzelm 2015-05-03 suppress formal sort-constraints, in accordance to norm_hhf_eqs;
2015-04-10 wenzelm 2015-04-10 tuned;
2015-03-31 wenzelm 2015-03-31 tuned signature;
2015-03-22 wenzelm 2015-03-22 tuned;
2015-03-20 wenzelm 2015-03-20 tuned -- prepare instantiation more uniformly;
2015-03-07 wenzelm 2015-03-07 clarified Drule.gen_all: observe context more carefully;
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 tuned signature;
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-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-04-06 wenzelm 2014-04-06 more source positions;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2013-06-27 wenzelm 2013-06-27 tuned signature;
2013-06-27 wenzelm 2013-06-27 tuned signature;
2013-05-29 wenzelm 2013-05-29 more precise "incremented" indication, which might be relevant in corner cases, e.g. instantiation of leading to vars with different types (which is a potential problem nonetheless);
2013-05-29 wenzelm 2013-05-29 tuned signature -- more explicit flags for low-level Thm.bicompose;