[isabelle] Simplification rule name for for (proving) equality of functions (has changed)

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.


Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Porto Alegre - RS - Brasil

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