Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. added inj_def (redundant, analogous to surj_def, bij_def); tuned proofs;
  2. tuned proofs;
  3. tuned proof;
  4. tuned whitespace;
  5. Added new / improved tactics for fields and rings
  6. Corrected type of dummy pattern
Changeset 64966:d53d7ca3303e by wenzelm:
added inj_def (redundant, analogous to surj_def, bij_def);<br>tuned proofs;
The file was modified src/HOL/Complete_Lattices.thy (diff)
The file was modified src/HOL/Fun.thy (diff)
The file was modified src/HOL/Library/Indicator_Function.thy (diff)
The file was modified src/HOL/Library/Permutations.thy (diff)
The file was modified src/HOL/List.thy (diff)
Changeset 64965:d55d743c45a2 by wenzelm:
tuned proofs;
The file was modified src/HOL/Fun.thy (diff)
Changeset 64964:a0c985a57f7e by wenzelm:
tuned proof;
The file was modified src/HOL/Power.thy (diff)
Changeset 64963:fc4d1ceb8e29 by wenzelm:
tuned whitespace;
The file was modified src/HOL/List.thy (diff)
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)