*** 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.

isabelle-dev mailing list

Reply via email to