Summary
- clarified prover-specific rules
- dropped potentially explosive rule for groebner simpset, with no observable effect on examples
- simplified fact references
- avoid effectively subsumed rules; simplified fact reference
The file was modified | src/HOL/Divides.thy (diff) |
The file was modified | src/HOL/Groebner_Basis.thy (diff) |
The file was modified | src/HOL/Groebner_Basis.thy (diff) |
The file was modified | src/HOL/Presburger.thy (diff) |