Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. prefer named lemmas -- more compact proofterms;
  2. more compact proofterms;
  3. eliminated pointless comments;
  4. clarified proofterms;
  5. more robust and convenient treatment of implicit context;
  6. removed junk (cf. fa933b98d64d);
  7. explicit check of left-over constraints from different theory, e.g. due to lack of Thm.trim_context;
  8. more careful treatment of implicit context;
  9. more careful treatment of implicit context;
  10. proper build options;
Changeset 70486:1dc3514c1719 by wenzelm:
prefer named lemmas -- more compact proofterms;
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/Tools/cnf.ML (diff)
Changeset 70485:b203aaf373cf by wenzelm:
more compact proofterms;
The file was modified src/HOL/Tools/Metis/metis_reconstruct.ML (diff)
Changeset 70484:63333b6a22c0 by wenzelm:
eliminated pointless comments;
The file was modified src/HOL/Tools/cnf.ML (diff)
Changeset 70483:59250a328113 by wenzelm:
clarified proofterms;
The file was modified src/HOL/Tools/typedef.ML (diff)
Changeset 70482:d4b5139eea34 by wenzelm:
more robust and convenient treatment of implicit context;
The file was modified src/Pure/thm.ML (diff)
Changeset 70481:d9ba9563b139 by wenzelm:
removed junk (cf. fa933b98d64d);
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 70480:1a1b7d7f24bb by wenzelm:
explicit check of left-over constraints from different theory, e.g. due to lack of Thm.trim_context;
The file was modified src/Pure/thm.ML (diff)
Changeset 70479:02d08d0ba896 by wenzelm:
more careful treatment of implicit context;
The file was modified src/HOL/Tools/Function/function_elims.ML (diff)
The file was modified src/HOL/Tools/Function/mutual.ML (diff)
Changeset 70478:94ed5be08e7f by wenzelm:
more careful treatment of implicit context;
The file was modified src/FOLP/simp.ML (diff)
Changeset 70477:90acc6ce5beb by wenzelm:
proper build options;
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)