[isabelle-dev] NEWS: Proof methods "simp" and "simp_all" in Pure
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