1.1 --- a/src/HOL/Orderings.thy	Wed Dec 08 13:34:50 2010 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Wed Dec 08 13:34:50 2010 +0100
     1.3 @@ -1214,13 +1214,13 @@
     1.4    less_bool_def: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
     1.5  
     1.6  definition
     1.7 -  top_bool_eq: "top = True"
     1.8 +  top_bool_def: "top = True"
     1.9  
    1.10  definition
    1.11 -  bot_bool_eq: "bot = False"
    1.12 +  bot_bool_def: "bot = False"
    1.13  
    1.14  instance proof
    1.15 -qed (auto simp add: bot_bool_eq top_bool_eq less_bool_def, auto simp add: le_bool_def)
    1.16 +qed (auto simp add: bot_bool_def top_bool_def less_bool_def, auto simp add: le_bool_def)
    1.17  
    1.18  end
    1.19  
    1.20 @@ -1237,10 +1237,10 @@
    1.21    by (simp add: le_bool_def)
    1.22  
    1.23  lemma bot_boolE: "bot \<Longrightarrow> P"
    1.24 -  by (simp add: bot_bool_eq)
    1.25 +  by (simp add: bot_bool_def)
    1.26  
    1.27  lemma top_boolI: top
    1.28 -  by (simp add: top_bool_eq)
    1.29 +  by (simp add: top_bool_def)
    1.30  
    1.31  lemma [code]:
    1.32    "False \<le> b \<longleftrightarrow> True"
    1.33 @@ -1276,11 +1276,11 @@
    1.34  begin
    1.35  
    1.36  definition
    1.37 -  top_fun_eq [no_atp]: "top = (\<lambda>x. top)"
    1.38 -declare top_fun_eq_raw [no_atp]
    1.39 +  top_fun_def [no_atp]: "top = (\<lambda>x. top)"
    1.40 +declare top_fun_def_raw [no_atp]
    1.41  
    1.42  instance proof
    1.43 -qed (simp add: top_fun_eq le_fun_def)
    1.44 +qed (simp add: top_fun_def le_fun_def)
    1.45  
    1.46  end
    1.47  
    1.48 @@ -1288,10 +1288,10 @@
    1.49  begin
    1.50  
    1.51  definition
    1.52 -  bot_fun_eq: "bot = (\<lambda>x. bot)"
    1.53 +  bot_fun_def: "bot = (\<lambda>x. bot)"
    1.54  
    1.55  instance proof
    1.56 -qed (simp add: bot_fun_eq le_fun_def)
    1.57 +qed (simp add: bot_fun_def le_fun_def)
    1.58  
    1.59  end
    1.60