# HG changeset patch
# User nipkow
# Date 1312786618 -7200
# Node ID f7634e2300bce581e588508b0e1f47dd0db14854
# Parent  9f9a40e778d6a758d9a39de00b87166d1b566d2e
removed old expand_fun_eq

diff -r 9f9a40e778d6 -r f7634e2300bc doc-src/TutorialI/Sets/sets.tex
--- a/doc-src/TutorialI/Sets/sets.tex	Mon Aug 08 08:25:28 2011 +0200
+++ b/doc-src/TutorialI/Sets/sets.tex	Mon Aug 08 08:56:58 2011 +0200
@@ -546,7 +546,7 @@
 equality over all arguments: 
 \begin{isabelle}
 (f\ =\ g)\ =\ ({\isasymforall}x.\ f\ x\ =\ g\ x)
-\rulename{expand_fun_eq}
+\rulename{fun_eq_iff}
 \end{isabelle}
 %
 This is just a restatement of
@@ -556,7 +556,7 @@
 function composition: 
 \begin{isabelle}
 \isacommand{lemma}\ "inj\ f\ \isasymLongrightarrow\ (f\ o\ g\ =\ f\ o\ h)\ =\ (g\ =\ h)"\isanewline
-\isacommand{apply}\ (simp\ add:\ expand_fun_eq\ inj_on_def)\isanewline
+\isacommand{apply}\ (simp\ add:\ fun_eq_iff\ inj_on_def)\isanewline
 \isacommand{apply}\ auto\isanewline
 \isacommand{done}
 \end{isabelle}