Skip to content
Success

Changes

Summary

  1. specific atomization inert to later rule set modifications
  2. more precise scope of atomize
  3. install simproc but deactivate by default
Changeset 71916:435cdc772110 by haftmann:
specific atomization inert to later rule set modifications
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)
Changeset 71915:3956d85e8e81 by haftmann:
more precise scope of atomize
The file was modified src/Provers/quantifier1.ML (diff)
Changeset 71914:3867734b9a40 by haftmann:
install simproc but deactivate by default
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/Library/Quantified_Premise_Simproc.thy (diff)