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

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
tuned;
2019-10-09, by wenzelm
misc tuning and clarification;
2019-10-09, by wenzelm
tuned;
2019-10-09, by wenzelm
tuned -- allow slightly more expensive atomic proofs;
2019-10-09, by wenzelm
clarified signature -- some operations to support fully explicit proof terms;
2019-10-09, by wenzelm
tuned;
2019-10-08, by wenzelm
tuned;
2019-10-08, by wenzelm
proper treatment of sorts;
2019-10-08, by wenzelm
tuned app_types: more direct map_proof_types_same;
2019-10-08, by wenzelm
tuned;
2019-10-08, by wenzelm
generalized parsing, for e.g. Leo-III
2019-10-09, by blanchet
More theorems about limits, including cancellation simprules
2019-10-09, by paulson
Generalised two results concerning limits from the real numbers to type classes
2019-10-09, by paulson
formally augmented corresponding rules for field_simps
2019-10-08, by haftmann
clarified option type;
2019-10-07, by wenzelm
count document nodes via raw file length;
2019-10-07, by wenzelm
merged
2019-10-07, by wenzelm
clarified Load_State / load_limit;
2019-10-07, by wenzelm
clarified Load_State;
2019-10-07, by wenzelm
discontinued pointless dump_checkpoint and share_common_data -- superseded by base logic image in Isabelle/MMT;
2019-10-07, by wenzelm
count nodes uniformly: avoid overloaded session;
2019-10-07, by wenzelm
clarified signature;
2019-10-07, by wenzelm
simplified proof
2019-10-07, by nipkow
tuned signature;
2019-10-06, by wenzelm

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

isabelle