Skip to content
Aborted

Changes

Summary

  1. added missing preprocessing step for extraction (due to Stefan Berghofer)
  2. new HOL simproc: eliminate_false_implies
  3. added lemma
Changeset 71843:07c85c68ff03 by manuel eberl _eberlm@in.tum.de_:
added missing preprocessing step for extraction (due to Stefan Berghofer)
The file was modified src/Pure/Proof/proof_rewrite_rules.ML (diff)
Changeset 71842:db120661dded by manuel eberl _eberlm@in.tum.de_:
new HOL simproc: eliminate_false_implies
The file was modified src/HOL/Analysis/Abstract_Topology_2.thy (diff)
The file was modified src/HOL/HOL.thy (diff)
Changeset 71841:f4626b1f1b96 by nipkow:
added lemma
The file was modified src/HOL/Nat.thy (diff)