Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more zproofs, underlying Proofterm.unconstrain_thm_proof / Thm.unconstrainT;
  2. omit syntactic of_class check, which is in conflict with sort constraints within the logic;
  3. tuned;
  4. minor performance tuning;
  5. clarified signature; clarified modules;
  6. misc tuning and clarification;
  7. tuned signature;
  8. tuned signature: canonical argument order;
Changeset 79429:637d7d896929 by wenzelm:
more zproofs, underlying Proofterm.unconstrain_thm_proof / Thm.unconstrainT;
The file was modified src/Pure/zterm.ML (diff)
Changeset 79428:4cd892d1a676 by wenzelm:
omit syntactic of_class check, which is in conflict with sort constraints within the logic;
The file was modified src/Pure/zterm.ML (diff)
Changeset 79427:6f852d23306a by wenzelm:
tuned;
The file was modified src/Pure/zterm.ML (diff)
Changeset 79426:b5ba5b767444 by wenzelm:
minor performance tuning;
The file was modified src/Pure/zterm.ML (diff)
Changeset 79425:0875c87b4a4b by wenzelm:
clarified signature;<br>clarified modules;
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
The file was modified src/Pure/zterm.ML (diff)
Changeset 79424:16c65e67dd75 by wenzelm:
misc tuning and clarification;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 79423:841545180269 by wenzelm:
tuned signature;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 79422:371ee5494d15 by wenzelm:
tuned signature: canonical argument order;
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/zterm.ML (diff)