Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. simplified a few proofs
  2. revisited ac28714b7478: more faithful preplaying with chained facts
  3. wait for E 2.7 before using 'ite' in HO mode
  4. added alternative E binary name
Changeset 73976:a5212df98387 by paulson _lp15@cam.ac.uk_:
simplified a few proofs
The file was modified src/HOL/Analysis/Finite_Cartesian_Product.thy (diff)
Changeset 73975:8d93f9ca6518 by blanchet:
revisited ac28714b7478: more faithful preplaying with chained facts
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML (diff)
Changeset 73974:6a0e1c14a8c2 by blanchet:
wait for E 2.7 before using 'ite' in HO mode
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)
Changeset 73973:f0d231ead660 by blanchet:
added alternative E binary name
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)