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

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

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

rewrite_proof: simplified simprocs (no name required);
adapted PThm;
fold_proof_atoms;

Thm.proof_of returns proof_body;
adapted PThm;

refined notion of derivation, consiting of promises and proof_body;
removed oracle_of (would require detailed check wrt. promises);
proof_of returns proof_body;

reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
added type proof_body, which covers oracles and thms of local proof;
added general fold_body_thms, fold_proof_atoms;
removed thms_of_proof, thms_of_proof', axms_of_proof;
slightly more abstract handling of body content (oracles, thms);
rewrite_proof: simplified simprocs (no name required);
thm_proof: lazy fulfillment of promises;

pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);

ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
adapted PThm;

name_of_thm: Proofterm.fold_proof_atoms;
Thm.proof_of returns proof_body;

Thm.proof_of returns proof_body;

clean: added HOL-Main;

rewrite_proof: simplified simprocs (no name required);