[isabelle] RC1: Basic_BNFs.snds



Hi,

induction on custom data types may still produce constants like
Basic_BNFs.snds, and these have no default simplifier setup. 
(I reported this behaviour to Dmitry privately some time ago, and just
stumbled over it accidentally, hoping it would long be fixed)

Things like thm Basic_BNFs.snds.simp should be in the default simpset,
or rules like 
"Basic_BNFs.snds (n, T) = {T}"

--
  Peter





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.