--- a/src/HOL/Data_Structures/Tree23_Set.thy Tue Jun 12 07:18:18 2018 +0200
+++ b/src/HOL/Data_Structures/Tree23_Set.thy Tue Jun 12 17:18:40 2018 +0200
@@ -11,6 +11,9 @@
declare sorted_wrt.simps(2)[simp del]
+definition empty :: "'a tree23" where
+"empty = Leaf"
+
fun isin :: "'a::linorder tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
"isin Leaf x = False" |
"isin (Node2 l a r) x =
@@ -377,7 +380,7 @@
subsection \<open>Overall Correctness\<close>
interpretation Set_by_Ordered
-where empty = Leaf and isin = isin and insert = insert and delete = delete
+where empty = empty and isin = isin and insert = insert and delete = delete
and inorder = inorder and inv = bal
proof (standard, goal_cases)
case 2 thus ?case by(simp add: isin_set)
@@ -389,6 +392,6 @@
case 6 thus ?case by(simp add: bal_insert)
next
case 7 thus ?case by(simp add: bal_delete)
-qed simp+
+qed (simp add: empty_def)+
end