# HG changeset patch
# User Andreas Lochbihler
# Date 1447256363 -3600
# Node ID 6fa23e7f08bd4a68e1e63e60e53fafe990071271
# Parent  6059ce322766f270b3d2d6c5a22fac574df70a5a# Parent  c657ee4f59b7edd84c34b8e06d81bb718ce49c17
merged

diff -r c657ee4f59b7 -r 6fa23e7f08bd src/HOL/Data_Structures/Splay_Set.thy
--- a/src/HOL/Data_Structures/Splay_Set.thy	Wed Nov 11 12:57:01 2015 +0100
+++ b/src/HOL/Data_Structures/Splay_Set.thy	Wed Nov 11 16:39:23 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)