Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. revived 'try0' and 'smart' Isar proofs in Sledgehammer
  2. Cleanup of NonstandardAnalysis
Changeset 75868:e7b04452eef3 by blanchet:
revived 'try0' and 'smart' Isar proofs in Sledgehammer
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML (diff)
Changeset 75867:d7595b12b9ea by paulson _lp15@cam.ac.uk_:
Cleanup of NonstandardAnalysis
The file was modified src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy (diff)