2019-10-15 wenzelm skip (somewhat pointless) shrink_proof more uniformly;
2019-10-15 wenzelm apply_preproc for all proof boxes;
2019-10-15 wenzelm cumulative errors for session partitions;
2019-10-15 wenzelm proper guard for process_theory: ensure uniform precedence of results;
2019-10-15 wenzelm load HOL-Proofs first: it introduces some extra "thm" items that are required later on;
2019-10-14 wenzelm clarified count_file;
2019-10-14 wenzelm clarified modules;
2019-10-14 wenzelm more complete coverage of sessions: process_theory operation needs to handle duplicate theories;
2019-10-14 wenzelm proper build_graph to make session selection work as in "isabelle build";
2019-10-14 wenzelm incorporate sessions with record_proofs;
2019-10-14 wenzelm clarified options;
2019-10-14 wenzelm clarified signature;
2019-10-14 wenzelm clarified signature;
2019-10-14 wenzelm clarified signature;
2019-10-14 wenzelm clarified signature;
2019-10-14 wenzelm clarified "isabelle update" options -- more like "isabelle dump";
2019-10-14 wenzelm clarified treatment of base logic image;
2019-10-14 wenzelm simplified options: always split;
2019-10-14 wenzelm proper guard -- avoid bad result;
2019-10-14 wenzelm split into standard partitions, for improved scalability;
2019-10-14 wenzelm clarified defaults;
2019-10-14 wenzelm tuned signature;
2019-10-14 wenzelm clarified signature: static Dump.Context vs. dynamic Dump.Session;
2019-10-13 wenzelm tuned signature;
2019-10-13 wenzelm tuned signature;
2019-10-13 wenzelm clarified sessions/directories;
2019-10-12 wenzelm clarified signature default;
2019-10-12 wenzelm clarified signature default;
2019-10-12 wenzelm more operations for type classes;
2019-10-12 wenzelm setup preprocessing for HOL proofs;
2019-10-12 wenzelm support preprocessing of exported proofs;
2019-10-12 wenzelm early setup of proof preprocessing;
2019-10-12 wenzelm clarified output and input of Typ/Term;
2019-10-12 wenzelm adapted to ML version;
2019-10-12 wenzelm more compact XML;
2019-10-12 wenzelm more compact XML: separate environment for free variables;
2019-10-12 wenzelm more compact XML;
2019-10-11 wenzelm merged
2019-10-11 wenzelm proper ML names;
2019-10-11 wenzelm clarified standard_proof_of: prefer expand_proof over somewhat adhoc strip_thm_proof;
2019-10-11 wenzelm some treatment of OfClass proofs;
2019-10-11 wenzelm tuned signature;
2019-10-11 wenzelm misc tuning and clarification;
2019-10-11 wenzelm proper treatment of axm_proof/oracle_proof like a closed proof constant, e.g. relevant for proof reconstruction of List.list.full_exhaustive_list.simps;
2019-10-11 wenzelm clarified oracle_proof;
2019-10-11 wenzelm tuned;
2019-10-11 wenzelm tuned;
2019-10-11 wenzelm tuned;
2019-10-11 wenzelm clarified signature;
2019-10-11 wenzelm tuned signature;
2019-10-10 wenzelm more compact XML representation;
2019-10-10 wenzelm proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
2019-10-10 wenzelm tuned;
2019-10-10 wenzelm tuned -- more direct ML expressions;
2019-10-10 wenzelm clarified modules;
2019-10-10 wenzelm tuned whitespace;
2019-10-10 wenzelm more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
2019-10-10 wenzelm unused;
2019-10-11 blanchet document antiquotations + clarify porting text slightly
2019-10-10 blanchet updated veriT part of Sledgehammer documentation
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip