Summary
- proper consideration of chained facts in 'try0' minimization
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff) |
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML (diff) |
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff) |
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML (diff) |