src/HOL/Library/ContNotDenum.thy

     "\<And>a b c::real. a < b \<Longrightarrow> i a b c < j a b c"
     "\<And>a b c. a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
     "\<And>a b c. a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
     by metis
 
-  def ivl \<equiv> "rec_nat (f 0 + 1, f 0 + 2) (\<lambda>n x. (i (fst x) (snd x) (f n), j (fst x) (snd x) (f n)))"
-  def I \<equiv> "\<lambda>n. {fst (ivl n) .. snd (ivl n)}"
+  define ivl where "ivl =
+    rec_nat (f 0 + 1, f 0 + 2) (\<lambda>n x. (i (fst x) (snd x) (f n), j (fst x) (snd x) (f n)))"
+  define I where "I n = {fst (ivl n) .. snd (ivl n)}" for n
 
   have ivl[simp]:
     "ivl 0 = (f 0 + 1, f 0 + 2)"
     "\<And>n. ivl (Suc n) = (i (fst (ivl n)) (snd (ivl n)) (f n), j (fst (ivl n)) (snd (ivl n)) (f n))"
     unfolding ivl_def by simp_all

 lemma bij_betw_open_intervals:
   fixes a b c d :: real
   assumes "a < b" "c < d"
   shows "\<exists>f. bij_betw f {a<..<b} {c<..<d}"
 proof -
-  def f \<equiv> "\<lambda>a b c d x::real. (d - c)/(b - a) * (x - a) + c"
+  define f where "f a b c d x = (d - c)/(b - a) * (x - a) + c" for a b c d x :: real
   { fix a b c d x :: real assume *: "a < b" "c < d" "a < x" "x < b"
     moreover from * have "(d - c) * (x - a) < (d - c) * (b - a)"
       by (intro mult_strict_left_mono) simp_all
     moreover from * have "0 < (d - c) * (x - a) / (b - a)"
       by simp