*** 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. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev