--- a/src/HOL/Library/Crude_Executable_Set.thy Sat Dec 05 20:02:21 2009 +0100
+++ b/src/HOL/Library/Crude_Executable_Set.thy Sun Dec 06 08:06:03 2009 +0100
@@ -236,12 +236,12 @@
lemma Inf_inf [code]:
"Inf (Set xs) = foldl inf (top :: 'a::complete_lattice) xs"
"Inf (Coset []) = (bot :: 'a::complete_lattice)"
- by (simp_all add: Inf_Univ bot_def [symmetric] Inf_set_fold)
+ by (simp_all add: Inf_UNIV Inf_set_fold)
lemma Sup_sup [code]:
"Sup (Set xs) = foldl sup (bot :: 'a::complete_lattice) xs"
"Sup (Coset []) = (top :: 'a::complete_lattice)"
- by (simp_all add: Sup_Univ top_def [symmetric] Sup_set_fold)
+ by (simp_all add: Sup_UNIV Sup_set_fold)
lemma Inter_inter [code]:
"Inter (Set xs) = foldl inter (Coset []) xs"