[isabelle-dev] NEWS: Proof methods "simp" and "simp_all" in Pure

Makarius makarius at sketis.net
Thu Jul 21 12:06:47 CEST 2016

*** General ***

* Pure provides basic versions of proof methods "simp" and "simp_all"
that only know about meta-equality (==). Potential INCOMPATIBILITY in
theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order
is relevant to avoid confusion of Pure.simp vs. HOL.simp.

This refers to Isabelle/b01154b74314. It means that "unfold" /
'unfolding' does not have to be abused for general simplification in
examples based on Pure.


More information about the isabelle-dev mailing list