1.1 --- a/src/HOL/Recdef.thy	Tue Feb 20 18:47:25 2001 +0100
     1.2 +++ b/src/HOL/Recdef.thy	Tue Feb 20 18:47:27 2001 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4    ("../TFL/post.ML")
     1.5    ("Tools/recdef_package.ML"):
     1.6  
     1.7 -lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
     1.8 +lemma tfl_some: "\\<forall>P x. P x --> P (Eps P)"
     1.9    by (blast intro: someI)
    1.10  
    1.11  lemma tfl_eq_True: "(x = True) --> x"
    1.12 @@ -35,13 +35,13 @@
    1.13  lemma tfl_imp_trans: "(A --> B) ==> (B --> C) ==> (A --> C)"
    1.14    by blast
    1.15  
    1.16 -lemma tfl_disj_assoc: "(a \<or> b) \<or> c == a \<or> (b \<or> c)"
    1.17 +lemma tfl_disj_assoc: "(a \\<or> b) \\<or> c == a \\<or> (b \\<or> c)"
    1.18    by simp
    1.19  
    1.20 -lemma tfl_disjE: "P \<or> Q ==> P --> R ==> Q --> R ==> R"
    1.21 +lemma tfl_disjE: "P \\<or> Q ==> P --> R ==> Q --> R ==> R"
    1.22    by blast
    1.23  
    1.24 -lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q"
    1.25 +lemma tfl_exE: "\\<exists>x. P x ==> \\<forall>x. P x --> Q ==> Q"
    1.26    by blast
    1.27  
    1.28  use "../TFL/utils.ML"
    1.29 @@ -61,8 +61,7 @@
    1.30    lex_prod_def
    1.31    less_Suc_eq [THEN iffD2]
    1.32  
    1.33 -lemmas [recdef_cong] =
    1.34 -  if_cong
    1.35 +lemmas [recdef_cong] = if_cong image_cong
    1.36  
    1.37  lemma let_cong [recdef_cong]:
    1.38      "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g"