Summary
- added missing preprocessing step for extraction (due to Stefan Berghofer)
- new HOL simproc: eliminate_false_implies
- added lemma
The file was modified | src/Pure/Proof/proof_rewrite_rules.ML (diff) |
The file was modified | src/HOL/Analysis/Abstract_Topology_2.thy (diff) |
The file was modified | src/HOL/HOL.thy (diff) |
The file was modified | src/HOL/Nat.thy (diff) |