Summary
- Added new / improved tactics for fields and rings
- Corrected type of dummy pattern
The file was added | src/HOL/Decision_Procs/Algebra_Aux.thy |
The file was added | src/HOL/Decision_Procs/Conversions.thy |
The file was added | src/HOL/Decision_Procs/Reflective_Field.thy |
The file was modified | src/HOL/Decision_Procs/Commutative_Ring.thy (diff) |
The file was modified | src/HOL/Decision_Procs/Commutative_Ring_Complete.thy (diff) |
The file was modified | src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy (diff) |
The file was removed | src/HOL/Decision_Procs/commutative_ring_tac.ML |
The file was modified | src/HOL/Tools/Ctr_Sugar/case_translation.ML (diff) |