Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. implicit eta contraction for preprocessed terms avoids unintended implicit eta expansion
  2. explicit operations for executable primality checks
  3. more fun without recdef
Changeset 65026:49c537d87896 by haftmann:
implicit eta contraction for preprocessed terms avoids unintended implicit eta expansion
The file was modified src/Tools/Code/code_preproc.ML (diff)
Changeset 65025:8c32ce2a01c6 by haftmann:
explicit operations for executable primality checks
The file was modified src/HOL/Number_Theory/Primes.thy (diff)
Changeset 65024:3cb801391353 by haftmann:
more fun without recdef
The file was modified src/HOL/Decision_Procs/Cooper.thy (diff)
The file was modified src/HOL/Tools/Qelim/cooper_procedure.ML (diff)