Summary
- merged
- de-applying and simplification
- datatype_record produces simp theorems; contributed in part by Yu Zhang
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) |
The file was modified | src/HOL/Library/datatype_records.ML (diff) |
The file was modified | src/HOL/ex/Datatype_Record_Examples.thy (diff) |