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

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
clarified signature: more options;
2019-10-06, by wenzelm
clarified signature: read full session requirements;
2019-10-06, by wenzelm
clarified signature;
2019-10-06, by wenzelm
tuned signature;
2019-10-06, by wenzelm
clarified options -- more scalable;
2019-10-05, by wenzelm
obsolete;
2019-10-04, by wenzelm
proper replacement for (map_types (K dummyT));
2019-10-04, by wenzelm
Term_XML.Encode/Decode.term uses Const "typargs";
2019-10-04, by wenzelm
prefer atomic edits -- potentially more robust;
2019-10-02, by wenzelm
clarified signature -- potentially more robust;
2019-10-02, by wenzelm
just one dump_checkpoint Main -- potentially more robust;
2019-10-02, by wenzelm
more robust: avoid update/interrupt of long-running print_consolidation;
2019-10-02, by wenzelm
avoid censorship of options, e.g. relevant for Isabelle/MMT to provide its own value;
2019-10-01, by wenzelm

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

isabelle