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