Skip to content
Success

Changes

Summary

  1. avoid using FOOL syntax with older Vampire versions because of soundness bug visible by passing 'Abs_unit_cases Rep_unit Rep_unit_cases' as the facts to Sledgehammer
  2. merged
  3. some refinements in Algebra and Number_Theory
  4. provide Go component
Changeset 78524:25f16c356dae by blanchet:
avoid using FOOL syntax with older Vampire versions because of soundness bug visible by passing 'Abs_unit_cases Rep_unit Rep_unit_cases' as the facts to Sledgehammer
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)
Changeset 78523:d96dd69903fb by paulson:
merged
Changeset 78522:918a9ed06898 by paulson _lp15@cam.ac.uk_:
some refinements in Algebra and Number_Theory
The file was modified src/HOL/Algebra/Ring.thy (diff)
The file was modified src/HOL/Number_Theory/Eratosthenes.thy (diff)
The file was modified src/HOL/Number_Theory/Residues.thy (diff)
Changeset 78521:8347ffa1f92c by lars hupel _lars.hupel@mytum.de_:
provide Go component
The file was addedAdmin/components/go