Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. de-applying and simplification
  3. datatype_record produces simp theorems; contributed in part by Yu Zhang
Changeset 68688:3a58abb11840 by paulson:
merged
Changeset 68687:2976a4a3b126 by paulson _lp15@cam.ac.uk_:
de-applying and simplification
The file was modified src/HOL/Algebra/Bij.thy (diff)
The file was modified src/HOL/Algebra/Coset.thy (diff)
The file was modified src/HOL/Algebra/Embedded_Algebras.thy (diff)
The file was modified src/HOL/Algebra/Generated_Groups.thy (diff)
The file was modified src/HOL/Algebra/Group.thy (diff)
The file was modified src/HOL/Algebra/Ideal.thy (diff)
The file was modified src/HOL/Algebra/RingHom.thy (diff)
The file was modified src/HOL/Library/FuncSet.thy (diff)
Changeset 68686:7f8db1c4ebec by lars hupel _lars.hupel@mytum.de_:
datatype_record produces simp theorems; contributed in part by Yu Zhang
The file was modified src/HOL/Library/datatype_records.ML (diff)
The file was modified src/HOL/ex/Datatype_Record_Examples.thy (diff)