Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. prefer named lemmas -- more compact proofterms;
  2. prefer named lemmas -- more compact proofterms;
  3. tuned whitespace -- slightly more readable;
  4. clarified signature: fewer warnings in ML IDE;
  5. tuned;
Changeset 70491:8cac53925407 by wenzelm:
prefer named lemmas -- more compact proofterms;
The file was modified src/HOL/Tools/Transfer/transfer.ML (diff)
The file was modified src/HOL/Transfer.thy (diff)
Changeset 70490:c42a0a0a9a8d by wenzelm:
prefer named lemmas -- more compact proofterms;
The file was modified src/HOL/Groups.thy (diff)
The file was modified src/HOL/Lattices.thy (diff)
The file was modified src/HOL/Nat.thy (diff)
The file was modified src/HOL/Tools/boolean_algebra_cancel.ML (diff)
The file was modified src/HOL/Tools/group_cancel.ML (diff)
The file was modified src/HOL/Tools/nat_arith.ML (diff)
Changeset 70489:12d1e6e2c1d0 by wenzelm:
tuned whitespace -- slightly more readable;
The file was modified src/HOL/Tools/Metis/metis_tactic.ML (diff)
Changeset 70488:c7ef6685c943 by wenzelm:
clarified signature: fewer warnings in ML IDE;
The file was modified src/HOL/Tools/Metis/metis_tactic.ML (diff)
Changeset 70487:9cb269b49cf7 by wenzelm:
tuned;
The file was modified src/HOL/Tools/Metis/metis_reconstruct.ML (diff)