summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 tip

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 tip

export constdefs according to defs.ML;

avoid spurious shyps (with vacous type variable);

merged

more robust hybrid treatment of Pure, notably for Isabelle/Dedukti;

clarified signature: name of standard_proof is authentic, otherwise empty;

clarified expand_proof/expand_name: allow more detailed control via thm_header;
export_standard_proofs: authentic theorem names in "print" format;

option to export standardized proof terms (not scalable);

more kinds, notably for Isabelle/MMT;

refined proof of concept for bit operations

more lemmas