src/HOL/Orderings.thy
changeset 41075 4bed56dc95fb
parent 38795 848be46708dc
child 41080 294956ff285b
--- a/src/HOL/Orderings.thy	Wed Dec 08 13:34:50 2010 +0100
+++ b/src/HOL/Orderings.thy	Wed Dec 08 13:34:50 2010 +0100
@@ -1214,13 +1214,13 @@
   less_bool_def: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
 
 definition
-  top_bool_eq: "top = True"
+  top_bool_def: "top = True"
 
 definition
-  bot_bool_eq: "bot = False"
+  bot_bool_def: "bot = False"
 
 instance proof
-qed (auto simp add: bot_bool_eq top_bool_eq less_bool_def, auto simp add: le_bool_def)
+qed (auto simp add: bot_bool_def top_bool_def less_bool_def, auto simp add: le_bool_def)
 
 end
 
@@ -1237,10 +1237,10 @@
   by (simp add: le_bool_def)
 
 lemma bot_boolE: "bot \<Longrightarrow> P"
-  by (simp add: bot_bool_eq)
+  by (simp add: bot_bool_def)
 
 lemma top_boolI: top
-  by (simp add: top_bool_eq)
+  by (simp add: top_bool_def)
 
 lemma [code]:
   "False \<le> b \<longleftrightarrow> True"
@@ -1276,11 +1276,11 @@
 begin
 
 definition
-  top_fun_eq [no_atp]: "top = (\<lambda>x. top)"
-declare top_fun_eq_raw [no_atp]
+  top_fun_def [no_atp]: "top = (\<lambda>x. top)"
+declare top_fun_def_raw [no_atp]
 
 instance proof
-qed (simp add: top_fun_eq le_fun_def)
+qed (simp add: top_fun_def le_fun_def)
 
 end
 
@@ -1288,10 +1288,10 @@
 begin
 
 definition
-  bot_fun_eq: "bot = (\<lambda>x. bot)"
+  bot_fun_def: "bot = (\<lambda>x. bot)"
 
 instance proof
-qed (simp add: bot_fun_eq le_fun_def)
+qed (simp add: bot_fun_def le_fun_def)
 
 end