Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more Isabelle/Haskell;
  2. made sure lambda-lifting works well with native let binders in Sledgehammer
  3. handle Zipperposition's ResourceOut gracefully
  4. disabled 'ite' in Zipperposition until we upgrade to a version of Zip that supports it and we generate the proper syntax
Changeset 74209:24a2a6ced0ab by wenzelm:
more Isabelle/Haskell;
The file was modified src/Tools/Haskell/Haskell.thy (diff)
Changeset 74208:1a8d8dd77513 by blanchet:
made sure lambda-lifting works well with native let binders in Sledgehammer
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (diff)
Changeset 74207:adf767b94f77 by blanchet:
handle Zipperposition's ResourceOut gracefully
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)
Changeset 74206:9c6159cbf9ee by blanchet:
disabled 'ite' in Zipperposition until we upgrade to a version of Zip that supports it and we generate the proper syntax
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)