Summary
- specific atomization inert to later rule set modifications
- more precise scope of atomize
- install simproc but deactivate by default
The file was modified | src/FOL/simpdata.ML (diff) |
The file was modified | src/HOL/Tools/simpdata.ML (diff) |
The file was modified | src/Provers/quantifier1.ML (diff) |
The file was modified | src/Provers/quantifier1.ML (diff) |
The file was modified | src/HOL/HOL.thy (diff) |
The file was modified | src/HOL/Library/Quantified_Premise_Simproc.thy (diff) |