Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. more diagnostic operations;
  3. tuned -- non-strict args;
  4. proper constrains_map -- for shyps that are covered by present variables (amending 251f1fb44ccd);
  5. tuned signature;
  6. clarified signature; tuned;
  7. tuned signature;
  8. News for bind infixl
  9. Monadic bind is now infixl as is the norm
Changeset 70441:52435af442a6 by wenzelm:
merged
Changeset 70440:03cfef16ddb4 by wenzelm:
more diagnostic operations;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70439:145fb19d906d by wenzelm:
tuned -- non-strict args;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70438:99024c9c83f6 by wenzelm:
proper constrains_map -- for shyps that are covered by present variables (amending 251f1fb44ccd);
The file was modified src/Pure/logic.ML (diff)
Changeset 70437:fdbb0c2e0162 by wenzelm:
tuned signature;
The file was modified src/Pure/logic.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70436:251f1fb44ccd by wenzelm:
clarified signature;<br>tuned;
The file was modified src/HOL/Types_To_Sets/internalize_sort.ML (diff)
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/Proof/reconstruct.ML (diff)
The file was modified src/Pure/logic.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70435:52fbcf7a61f8 by wenzelm:
tuned signature;
The file was modified src/HOL/Types_To_Sets/internalize_sort.ML (diff)
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/Proof/reconstruct.ML (diff)
The file was modified src/Pure/logic.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70434:4abd07cd034f by nipkow:
News for bind infixl
The file was modified NEWS (diff)
Changeset 70433:2137db107788 by nipkow:
Monadic bind is now infixl as is the norm
The file was modified src/HOL/Library/Monad_Syntax.thy (diff)