Summary
- removal of needless hypothesis in hd_rev and last_rev
The file was modified | src/HOL/Computational_Algebra/Polynomial.thy (diff) |
The file was modified | src/HOL/List.thy (diff) |
The file was modified | src/HOL/Computational_Algebra/Polynomial.thy (diff) |
The file was modified | src/HOL/List.thy (diff) |