more zproofs;

more operations;

clarified modules; minor performance tuning;

minor performance tuning, following 703201dbd413;

tuned;

clarified signature: suppress unused fields;

eliminate clone (amending e7796c55d840);

minor performance tuning;

more operations;

more operations;

tuned;

clarified store_proof: before attributes are applied, to ensure proper thm_proof boxes for declaration attributes;

tuned;

tuned signature;

tuned; more uniform Thm.transfer;

tuned;

more accurate Global_Theory.name_facts: burrow into expression of attributed theorems;

clarified modules;

clarified signature;

tuned;

clarified Global_Theory.store_proofs vs. Generic_Target.thm_definition / Attrib.global_notes;

clarified signature;

tuned;

tuned: avoid duplicates;

more operations;

proper Thm.transfer;

proper Thm.trim_context;

clarified stored data: actual thm allows to replay zproofs in a modular manner;

tuned signature;

tuned signature, following Proofterm.thm_header;

more robust: avoid crash of Thm.solve_constraints due to changed background theory, e.g. relevant for AFP/Transition_Systems_and_Automata;

clarified signature;

proper Thm_Name.make_list for thm_definition; tuned modules;

more robust: avoid crash of AFP/Transition_Systems_and_Automata (amending fe4bd39bfeac and 43d8385db923);

more robust: zproofs need to be enabled (amending 43d8385db923);

more thorough thm definition via Global_Theory.register_proofs: store (and purge) zproofs;

tuned names;

clarified signature: support update of local_theory;

tuned;

clarified modules;

tuned;

unused;

clarified modules;

tuned;

clarified modules;

tuned;

tuned signature;

tuned;

more operations;

eliminate duplicate (see also 6cbcfac5b72e and af7b79271364);

minor performance tuning: shorter names;

minor performance tuning: static vs. dynamic rules;

minor performance tuning;

clarified signature: downgrade old-style Global_Theory.add_defs to Global_Theory.add_def without attributes;

clarified signature;

tuned;

more thorough treatment of zproof vs. proof: avoid accidental storage of large structures;

clarified signature;

observe option "prune_proofs";

clarified zproof storage: per-theory table in anticipation of session exports;

proper thm_name for stored zproof;

uniform treatment of lazy facts: actual proof terms are always strict;

tuned;

tuned whitespace;

tuned;

proper Thm.transfer;

clarified context: avoid capture of thy2 within closure;

tuned names;

more informative exceptions;

more permissive: allow collapse of term variables for equal results, e.g. relevant for metis (line 1882 of "~~/src/HOL/List.thy");

tuned;

more informative exception;

clarified signature;

clarified ML toplevel output: avoid "??." prefix;

tuned;

merged

use strict Global_Theory.register_proofs as checkpoint for stored zproof, and thus reduce current zboxes;

clarified signature;

omit pointless future: proof terms are built sequentially;

omit unclear / inaccurate renaming;

more normalization: re-use Thm.solve_constraints as important checkpoint for results, notably Global_Theory.name_thm;

more robust: avoid assumption about Context.certificate_theory;

tuned;

clarified pro-forma proof: no zboxes here (partially revert 686b7b14d041);

tuned;

tuned;

more normalization;

less ambitious normalization: term abstractions over terms and proofs, but not proofs over proofs (which may be large);

tuned;

more thorough beta contraction, following Envir.norm_term;

tuned, following Envir.norm_term;

more operations;

merged

unused lemma

restore benchmark requirement heaps properly;

continue build while waiting for updated schedule;