# HG changeset patch
# User nipkow
# Date 1447252861 -3600
# Node ID 6059ce322766f270b3d2d6c5a22fac574df70a5a
# Parent  c304402cc3df3699a290c2f764ffc3701faa9f41
tuned

diff -r c304402cc3df -r 6059ce322766 src/HOL/Data_Structures/Splay_Set.thy
--- a/src/HOL/Data_Structures/Splay_Set.thy	Tue Nov 10 23:41:20 2015 +0100
+++ b/src/HOL/Data_Structures/Splay_Set.thy	Wed Nov 11 15:41:01 2015 +0100
@@ -136,7 +136,7 @@
 
 subsubsection "Proofs for insert"
 
-(* more sorted lemmas; unify with basic set? *)
+text\<open>Splay trees need two addition @{const sorted} lemmas:\<close>
 
 lemma sorted_snoc_le:
   "ASSUMPTION(sorted(xs @ [x])) \<Longrightarrow> x \<le> y \<Longrightarrow> sorted (xs @ [y])"
@@ -157,6 +157,8 @@
 by(induction x t arbitrary: l a r rule: splay.induct)
   (auto simp: sorted_lems sorted_Cons_le sorted_snoc_le splay_Leaf_iff split: tree.splits)
 
+text\<open>Splay trees need two addition @{const ins_list} lemmas:\<close>
+
 lemma ins_list_Cons: "sorted (x # xs) \<Longrightarrow> ins_list x xs = x # xs"
 by (induction xs) auto
 
@@ -171,7 +173,7 @@
 
 subsubsection "Proofs for delete"
 
-(* more del_simp lemmas; unify with basic set? *)
+text\<open>Splay trees need two addition @{const del_list} lemmas:\<close>
 
 lemma del_list_notin_Cons: "sorted (x # xs) \<Longrightarrow> del_list x xs = xs"
 by(induction xs)(auto simp: sorted_Cons_iff)