Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. tuned name
  3. new simplifier trace_op for tracing simproc calls
  4. merged
  5. Some new material about Ramsey's theorem, also sharpening the proof to deliver the Erdős–Szekeres upper bound on Ramsey numbers
  6. support Zipperposition's skolemization in generated Isar proofs
  7. improved output in simps_case_conv;
  8. improved output in inductive module;
  9. simplifier: no trace info from simprocs unless simp_debug = true.
Changeset 79739:407f201b7f22 by nipkow:
merged
Changeset 79738:8ae4fc4692e8 by nipkow:
tuned name
The file was modified src/Pure/raw_simplifier.ML (diff)
Changeset 79737:9c00a46d69d0 by nipkow:
new simplifier trace_op for tracing simproc calls
The file was modified src/Pure/Tools/simplifier_trace.ML (diff)
The file was modified src/Pure/raw_simplifier.ML (diff)
Changeset 79736:1f7c8065f6a1 by paulson:
merged
Changeset 79735:d11cee9c3a7c by paulson _lp15@cam.ac.uk_:
Some new material about Ramsey's theorem, also sharpening the proof to deliver the Erdős–Szekeres upper bound on Ramsey numbers
The file was modified src/HOL/Library/Ramsey.thy (diff)
Changeset 79734:0fa4bebbdd75 by blanchet:
support Zipperposition's skolemization in generated Isar proofs
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_proof_reconstruct.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)
Changeset 79733:3e30ca77ccfe by fabian huch _huch@in.tum.de_:
improved output in simps_case_conv;
The file was modified src/HOL/Library/simps_case_conv.ML (diff)
Changeset 79732:a53287d9add3 by fabian huch _huch@in.tum.de_:
improved output in inductive module;
The file was modified src/HOL/Tools/inductive.ML (diff)
Changeset 79731:6dbe7910dcfc by nipkow:
simplifier: no trace info from simprocs unless simp_debug = true.
The file was modified src/Doc/Isar_Ref/Generic.thy (diff)
The file was modified src/Pure/raw_simplifier.ML (diff)