Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. generalised pigeonhole principle in HOL-Library.FuncSet
  2. new constant power_int in HOL
  3. New HOL simproc 'datatype_no_proper_subterm'
Changeset 71838:5656ec95493c by manuel eberl _eberlm@in.tum.de_:
generalised pigeonhole principle in HOL-Library.FuncSet
The file was modified src/HOL/Library/FuncSet.thy (diff)
Changeset 71837:dca11678c495 by manuel eberl _eberlm@in.tum.de_:
new constant power_int in HOL
The file was modified NEWS (diff)
The file was modified src/HOL/Deriv.thy (diff)
The file was modified src/HOL/Int.thy (diff)
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/Parity.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
Changeset 71836:c095d3143047 by manuel eberl _eberlm@in.tum.de_:
New HOL simproc 'datatype_no_proper_subterm'
The file was addedsrc/HOL/Datatype_Examples/Datatype_Simproc_Tests.thy
The file was addedsrc/HOL/Tools/datatype_simprocs.ML
The file was modified NEWS (diff)
The file was modified src/HOL/BNF_Least_Fixpoint.thy (diff)
The file was modified src/HOL/Hoare_Parallel/RG_Hoare.thy (diff)
The file was modified src/HOL/Nat.thy (diff)
The file was modified src/HOL/ROOT (diff)