Email Gateway (Aug 18 2022 at 18:23): Email Gateway (Aug 18 2022 at 18:23):From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
Isabelle 2011 não does recognize the now old and famous simplification rule
"expand_fun_eq" (from
Fun theory)
as Isabelle 2009-2 does. It gives the message "Unknown fact", etc. Looking
in the Fun theory one sees that
its name has changed to "fun_eq_iff". However, the 2011 tutorial still uses
the old name. It is not
a big deal, but I think it is better to update the tutorial in this sense.
Best!
Last updated: Apr 20 2024 at 08:16 UTC