Skip to content
Failed

Changes

Summary

  1. clarified prover-specific rules
  2. dropped potentially explosive rule for groebner simpset, with no observable effect on examples
  3. simplified fact references
  4. avoid effectively subsumed rules; simplified fact reference
Changeset 64250:0cde0b4d4cb5 by haftmann:
clarified prover-specific rules
The file was modified src/HOL/Divides.thy (diff)
Changeset 64249:a3f654f9a46c by haftmann:
dropped potentially explosive rule for groebner simpset, with no observable effect on examples
The file was modified src/HOL/Groebner_Basis.thy (diff)
Changeset 64248:690eb1ae8bb0 by haftmann:
simplified fact references
The file was modified src/HOL/Groebner_Basis.thy (diff)
Changeset 64247:f537616459e6 by haftmann:
avoid effectively subsumed rules;<br>simplified fact reference
The file was modified src/HOL/Presburger.thy (diff)