# HG changeset patch
# User haftmann
# Date 1284987045 -7200
# Node ID e7d4923b9b1c9f47558eb3e25d34d4bde6c5a363
# Parent  baa049cba98b627cedbf45a7b5dd8407ba57f1f4
expand_fun_eq -> fun_eq_iff

diff -r baa049cba98b -r e7d4923b9b1c doc-src/Codegen/Thy/Further.thy
--- 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
diff -r baa049cba98b -r e7d4923b9b1c doc-src/Codegen/Thy/document/Further.tex
--- 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}%
 %