removed old expand_fun_eq
authornipkow
Mon, 08 Aug 2011 08:56:58 +0200
changeset 44050 f7634e2300bc
parent 44049 9f9a40e778d6
child 44051 2ec66075a75c
removed old expand_fun_eq
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}