src/Pure/thm.ML
6 months ago wenzelm clarified signature: more operations;
6 months ago wenzelm tuned signature;
7 months ago wenzelm more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
7 months ago wenzelm tuned signature;
12 months ago wenzelm more uniform treatment of "hyps" within zproof;
12 months ago wenzelm clarified signature: avoid redundant Term.maxidx_of_term;
12 months ago wenzelm tuned signature;
12 months ago wenzelm tuned signature;
12 months ago wenzelm clarified signature;
12 months ago wenzelm more operations (see also 8368160d3c65);
12 months ago wenzelm clarified signature;
12 months ago wenzelm tuned signature;
12 months ago wenzelm minor performance tuning: proper Same.operation;
12 months ago wenzelm pro-forma support for ZTerm.sorts_zproof;
12 months ago wenzelm tuned comments;
12 months ago wenzelm minor performance tuning: proper Same.operation;
12 months ago wenzelm tuned names (again);
12 months ago wenzelm tuned names;
12 months ago wenzelm clarified signature;
12 months ago wenzelm tuned;
12 months ago wenzelm clarified signature;
12 months ago wenzelm more zproofs;
12 months ago wenzelm clarified modules;
12 months ago wenzelm minor performance tuning, following 703201dbd413;
13 months ago wenzelm more operations;
13 months ago wenzelm proper Thm.transfer;
13 months ago wenzelm proper Thm.trim_context;
13 months ago wenzelm clarified stored data: actual thm allows to replay zproofs in a modular manner;
13 months ago wenzelm clarified signature;
13 months ago wenzelm clarified signature;
13 months ago wenzelm observe option "prune_proofs";
13 months ago wenzelm clarified zproof storage: per-theory table in anticipation of session exports;
13 months ago wenzelm proper thm_name for stored zproof;
13 months ago wenzelm clarified context: avoid capture of thy2 within closure;
13 months ago wenzelm tuned names;
13 months ago wenzelm more informative exceptions;
13 months ago wenzelm use strict Global_Theory.register_proofs as checkpoint for stored zproof, and thus reduce current zboxes;
13 months ago wenzelm omit unclear / inaccurate renaming;
13 months ago wenzelm more normalization: re-use Thm.solve_constraints as important checkpoint for results, notably Global_Theory.name_thm;
13 months ago wenzelm more robust: avoid assumption about Context.certificate_theory;
13 months ago wenzelm tuned;
13 months ago wenzelm clarified pro-forma proof: no zboxes here (partially revert 686b7b14d041);
13 months ago wenzelm tuned;
13 months ago wenzelm tuned;
13 months ago wenzelm minor performance tuning: more concise union;
13 months ago wenzelm clarified signature;
13 months ago wenzelm more robust norm_proof: turn env into instantiation, based on visible statement;
13 months ago wenzelm clarified signature;
13 months ago wenzelm clarified modules;
13 months ago wenzelm more zproofs;
13 months ago wenzelm more zproofs, imitating existing proofs (which are a bit rough here);
13 months ago wenzelm tuned whitespace;
13 months ago wenzelm minor performance tuning;
13 months ago wenzelm tuned comments (see also 476a239d3e0e and possibly 4b62e0cb3aa8);
13 months ago wenzelm minor performance tuning;
13 months ago wenzelm tuned;
13 months ago wenzelm minor performance tuning: prefer Same.operation;
13 months ago wenzelm clarified signature;
13 months ago wenzelm misc tuning and clarification;
13 months ago wenzelm minor performance tuning: prefer Symset.T;
less more (0) -300 -100 -60 tip