isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip

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

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip

isabelle