Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified generic euclidean relation
  2. added a bound in SMT on the number of schematic constants considered -- the code (in for_schematics) is exponential in that number
Changeset 76053:3310317cc484 by haftmann:
clarified generic euclidean relation
The file was modified src/HOL/Code_Numeral.thy (diff)
The file was modified src/HOL/Divides.thy (diff)
The file was modified src/HOL/Euclidean_Division.thy (diff)
Changeset 76052:6a20d0ebd5b3 by blanchet:
added a bound in SMT on the number of schematic constants considered -- the code (in for_schematics) is exponential in that number
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML (diff)
The file was modified src/HOL/Tools/monomorph.ML (diff)