--- a/src/HOL/Finite_Set.thy Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Finite_Set.thy Mon Apr 25 16:09:26 2016 +0200
@@ -919,7 +919,7 @@
case 0 then show ?case by simp
next
case (Suc n g)
- def h \<equiv> "\<lambda>z. g z - 1"
+ define h where "h z = g z - 1" for z
with Suc have "n = h y" by simp
with Suc have hyp: "f y ^^ h y \<circ> f x = f x \<circ> f y ^^ h y"
by auto
@@ -927,7 +927,7 @@
then show ?case by (simp add: comp_assoc hyp)
(simp add: o_assoc comp_fun_commute)
qed
- def h \<equiv> "\<lambda>z. if z = x then g x - 1 else g z"
+ define h where "h z = (if z = x then g x - 1 else g z)" for z
with Suc have "n = h x" by simp
with Suc have "f y ^^ h y \<circ> f x ^^ h x = f x ^^ h x \<circ> f y ^^ h y"
by auto