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

* Isar: the assumptions of a long theorem statement are available as assms;

activated x86_64-linux;

renamed Proof.put_thms_internal to Proof.put_thms;

simplified Proof.theorem(_i);
moved theorem kinds from PureThy to Thm;

added stmt mode, which affects naming/indexing of local facts;
renamed put_thms_internal to put_thms;
notes: proper name and kind (outside of proof body);
removed dead code;

simplified theorem(_i);
notes: proper kind;
renamed put_thms_internal to put_thms;

notes: proper kind;
simplified Proof.theorem(_i);
context_statement: ProofContext.set_stmt after import;

notes: proper kind;

removed kind attribs;

moved theorem kinds from PureThy to Thm;
exported note_thms(s);