--- a/doc-src/Codegen/Thy/Further.thy Mon Sep 20 14:36:54 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy Mon Sep 20 14:50:45 2010 +0200
@@ -103,7 +103,7 @@
interpretation %quote fun_power: power "\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n" where
"power.powers (\<lambda>n f. f ^^ n) = funpows"
by unfold_locales
- (simp_all add: expand_fun_eq funpow_mult mult_commute funpows_def)
+ (simp_all add: fun_eq_iff funpow_mult mult_commute funpows_def)
text {*
\noindent This additional equation is trivially proved by the definition
--- a/doc-src/Codegen/Thy/document/Further.tex Mon Sep 20 14:36:54 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex Mon Sep 20 14:50:45 2010 +0200
@@ -191,7 +191,7 @@
\ \ {\isachardoublequoteopen}power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ f{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}\ {\isacharequal}\ funpows{\isachardoublequoteclose}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ unfold{\isacharunderscore}locales\isanewline
-\ \ \ \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq\ funpow{\isacharunderscore}mult\ mult{\isacharunderscore}commute\ funpows{\isacharunderscore}def{\isacharparenright}%
+\ \ \ \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ fun{\isacharunderscore}eq{\isacharunderscore}iff\ funpow{\isacharunderscore}mult\ mult{\isacharunderscore}commute\ funpows{\isacharunderscore}def{\isacharparenright}%
\endisatagquote
{\isafoldquote}%
%