Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tiny renaming
  2. merged
  3. Added the multiset termination proof
  4. generate some metainformation not only for SPASS but also for Zipperposition, for experimentation
Changeset 76304:e5162a8baa24 by paulson _lp15@cam.ac.uk_:
tiny renaming
The file was modified src/HOL/Examples/Ackermann.thy (diff)
Changeset 76303:f89f4aab1cc4 by paulson:
merged
Changeset 76302:8d2bf9ce5302 by paulson _lp15@cam.ac.uk_:
Added the multiset termination proof
The file was modified src/HOL/Examples/Ackermann.thy (diff)
Changeset 76301:73b120e0dbfe by blanchet:
generate some metainformation not only for SPASS but also for Zipperposition, for experimentation
The file was modified src/HOL/Tools/ATP/atp_problem.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)