Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Added new / improved tactics for fields and rings
  2. Corrected type of dummy pattern
Changeset 64962:bf41e1109db3 by berghofe:
Added new / improved tactics for fields and rings
The file was addedsrc/HOL/Decision_Procs/Algebra_Aux.thy
The file was addedsrc/HOL/Decision_Procs/Conversions.thy
The file was addedsrc/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 removedsrc/HOL/Decision_Procs/commutative_ring_tac.ML
Changeset 64961:d19a5579ffb8 by berghofe:
Corrected type of dummy pattern
The file was modified src/HOL/Tools/Ctr_Sugar/case_translation.ML (diff)