# HG changeset patch
# User eberlm
# Date 1446461798 -3600
# Node ID e3984606b4b6f20ffa074005157f5879699528f4
# Parent  ab2e862263e72484dd964bd873bb1bb741e6fda5# Parent  aa1ece0bce629deaff7f0050fd72a5f08ec98e43
Merged

diff -r ab2e862263e7 -r e3984606b4b6 NEWS
--- a/NEWS	Mon Nov 02 11:56:28 2015 +0100
+++ b/NEWS	Mon Nov 02 11:56:38 2015 +0100
@@ -66,6 +66,10 @@
 uniformly, and allow the dummy file argument ":" to open an empty buffer
 instead.
 
+* The default look-and-feel for Linux is the traditional "Metal", which
+works better with GUI scaling for very high-resolution displays (e.g.
+4K). Moreover, it is generally more robust than "Nimbus".
+
 
 *** Document preparation ***
 
diff -r ab2e862263e7 -r e3984606b4b6 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Mon Nov 02 11:56:28 2015 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Mon Nov 02 11:56:38 2015 +0100
@@ -283,7 +283,7 @@
   Isabelle/jEdit enables platform-specific look-and-feel by default as
   follows.
 
-  \<^descr>[Linux:] The platform-independent \<^emph>\<open>Nimbus\<close> is used by
+  \<^descr>[Linux:] The platform-independent \<^emph>\<open>Metal\<close> is used by
   default.
 
   \<^emph>\<open>GTK+\<close> also works under the side-condition that the overall GTK theme
@@ -310,7 +310,7 @@
   Users may experiment with different look-and-feels, but need to keep
   in mind that this extra variance of GUI functionality is unlikely to
   work in arbitrary combinations.  The platform-independent
-  \<^emph>\<open>Nimbus\<close> and \<^emph>\<open>Metal\<close> should always work.  The historic
+  \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close> should always work.  The historic
   \<^emph>\<open>CDE/Motif\<close> should be ignored.
 
   After changing the look-and-feel in \<^emph>\<open>Global Options~/
@@ -353,7 +353,7 @@
 
   \<^item> \<^emph>\<open>Global Options / Appearance / Button, menu and label font\<close> as
   well as \<^emph>\<open>List and text field font\<close>: this specifies the primary and
-  secondary font for the old \<^emph>\<open>Metal\<close> look-and-feel
+  secondary font for the traditional \<^emph>\<open>Metal\<close> look-and-feel
   (\secref{sec:look-and-feel}), which happens to scale better than newer ones
   like \<^emph>\<open>Nimbus\<close>.
 
diff -r ab2e862263e7 -r e3984606b4b6 src/HOL/Data_Structures/Splay_Map.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Splay_Map.thy	Mon Nov 02 11:56:38 2015 +0100
@@ -0,0 +1,180 @@
+(* Author: Tobias Nipkow *)
+
+section "Splay Tree Implementation of Maps"
+
+theory Splay_Map
+imports
+  Splay_Set
+  Map_by_Ordered
+begin
+
+function splay :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
+"splay x Leaf = Leaf" |
+"x = fst a \<Longrightarrow> splay x (Node t1 a t2) = Node t1 a t2" |
+"x = fst a \<Longrightarrow> x < fst b \<Longrightarrow> splay x (Node (Node t1 a t2) b t3) = Node t1 a (Node t2 b t3)" |
+"x < fst a \<Longrightarrow> splay x (Node Leaf a t) = Node Leaf a t" |
+"x < fst a \<Longrightarrow> x < fst b \<Longrightarrow> splay x (Node (Node Leaf a t1) b t2) = Node Leaf a (Node t1 b t2)" |
+"x < fst a \<Longrightarrow> x < fst b \<Longrightarrow> t1 \<noteq> Leaf \<Longrightarrow>
+ splay x (Node (Node t1 a t2) b t3) =
+ (case splay x t1 of Node t11 y t12 \<Rightarrow> Node t11 y (Node t12 a (Node t2 b t3)))" |
+"fst a < x \<Longrightarrow> x < fst b \<Longrightarrow> splay x (Node (Node t1 a Leaf) b t2) = Node t1 a (Node Leaf b t2)" |
+"fst a < x \<Longrightarrow> x < fst b \<Longrightarrow> t2 \<noteq> Leaf \<Longrightarrow>
+ splay x (Node (Node t1 a t2) b t3) =
+ (case splay x t2 of Node t21 y t22 \<Rightarrow> Node (Node t1 a t21) y (Node t22 b t3))" |
+"fst a < x \<Longrightarrow> x = fst b \<Longrightarrow> splay x (Node t1 a (Node t2 b t3)) = Node (Node t1 a t2) b t3" |
+"fst a < x \<Longrightarrow> splay x (Node t a Leaf) = Node t a Leaf" |
+"fst a < x \<Longrightarrow> x < fst b \<Longrightarrow>  t2 \<noteq> Leaf \<Longrightarrow>
+ splay x (Node t1 a (Node t2 b t3)) =
+ (case splay x t2 of Node t21 y t22 \<Rightarrow> Node (Node t1 a t21) y (Node t22 b t3))" |
+"fst a < x \<Longrightarrow> x < fst b \<Longrightarrow> splay x (Node t1 a (Node Leaf b t2)) = Node (Node t1 a Leaf) b t2" |
+"fst a < x \<Longrightarrow> fst b < x \<Longrightarrow> splay x (Node t1 a (Node t2 b Leaf)) = Node (Node t1 a t2) b Leaf" |
+"fst a < x \<Longrightarrow> fst b < x \<Longrightarrow> t3 \<noteq> Leaf \<Longrightarrow>
+ splay x (Node t1 a (Node t2 b t3)) =
+ (case splay x t3 of Node t31 y t32 \<Rightarrow> Node (Node (Node t1 a t2) b t31) y t32)"
+apply(atomize_elim)
+apply(auto)
+(* 1 subgoal *)
+apply (subst (asm) neq_Leaf_iff)
+apply(auto)
+apply (metis tree.exhaust surj_pair less_linear)+
+done
+
+termination splay
+by lexicographic_order
+
+lemma splay_code: "splay x t = (case t of Leaf \<Rightarrow> Leaf |
+  Node al a ar \<Rightarrow>
+  (if x = fst a then t else
+   if x < fst a then
+     case al of
+       Leaf \<Rightarrow> t |
+       Node bl b br \<Rightarrow>
+         (if x = fst b then Node bl b (Node br a ar) else
+          if x < fst b then
+            if bl = Leaf then Node bl b (Node br a ar)
+            else case splay x bl of
+                   Node bll y blr \<Rightarrow> Node bll y (Node blr b (Node br a ar))
+          else
+          if br = Leaf then Node bl b (Node br a ar)
+          else case splay x br of
+                 Node brl y brr \<Rightarrow> Node (Node bl b brl) y (Node brr a ar))
+   else
+   case ar of
+     Leaf \<Rightarrow> t |
+     Node bl b br \<Rightarrow>
+       (if x = fst b then Node (Node al a bl) b br else
+        if x < fst b then
+          if bl = Leaf then Node (Node al a bl) b br
+          else case splay x bl of
+                 Node bll y blr \<Rightarrow> Node (Node al a bll) y (Node blr b br)
+        else if br=Leaf then Node (Node al a bl) b br
+             else case splay x br of
+                    Node bll y blr \<Rightarrow> Node (Node (Node al a bl) b bll) y blr)))"
+by(auto split: tree.split)
+
+definition lookup :: "('a*'b)tree \<Rightarrow> 'a::linorder \<Rightarrow> 'b option" where "lookup t x =
+  (case splay x t of Leaf \<Rightarrow> None | Node _ (a,b) _ \<Rightarrow> if x=a then Some b else None)"
+
+hide_const (open) insert
+
+fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
+"update x y t =  (if t = Leaf then Node Leaf (x,y) Leaf
+  else case splay x t of
+    Node l a r \<Rightarrow> if x = fst a then Node l (x,y) r
+      else if x < fst a then Node l (x,y) (Node Leaf a r) else Node (Node l a Leaf) (x,y) r)"
+
+definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
+"delete x t = (if t = Leaf then Leaf
+  else case splay x t of Node l a r \<Rightarrow>
+    if x = fst a
+    then if l = Leaf then r else case splay_max l of Node l' m r' \<Rightarrow> Node l' m r
+    else Node l a r)"
+
+
+subsection "Functional Correctness Proofs"
+
+lemma splay_Leaf_iff: "(splay x t = Leaf) = (t = Leaf)"
+by(induction x t rule: splay.induct) (auto split: tree.splits)
+
+
+subsubsection "Proofs for lookup"
+
+lemma splay_map_of_inorder:
+  "splay x t = Node l a r \<Longrightarrow> sorted1(inorder t) \<Longrightarrow>
+   map_of (inorder t) x = (if x = fst a then Some(snd a) else None)"
+by(induction x t arbitrary: l a r rule: splay.induct)
+  (auto simp: map_of_simps splay_Leaf_iff split: tree.splits)
+
+lemma lookup_eq:
+  "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
+by(auto simp: lookup_def splay_Leaf_iff splay_map_of_inorder split: tree.split)
+
+
+subsubsection "Proofs for update"
+
+lemma inorder_splay: "inorder(splay x t) = inorder t"
+by(induction x t rule: splay.induct)
+  (auto simp: neq_Leaf_iff split: tree.split)
+
+lemma sorted_splay:
+  "sorted1(inorder t) \<Longrightarrow> splay x t = Node l a r \<Longrightarrow>
+  sorted(map fst (inorder l) @ x # map fst (inorder r))"
+unfolding inorder_splay[of x t, symmetric]
+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)
+
+(* more upd_list lemmas; unify with basic set? *)
+
+lemma upd_list_Cons:
+  "sorted1 ((x,y) # xs) \<Longrightarrow> upd_list x y xs = (x,y) # xs"
+by (induction xs) auto
+
+lemma upd_list_snoc:
+  "sorted1 (xs @ [(x,y)]) \<Longrightarrow> upd_list x y xs = xs @ [(x,y)]"
+by(induction xs) (auto simp add: sorted_mid_iff2)
+
+lemma inorder_update:
+  "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
+using inorder_splay[of x t, symmetric] sorted_splay[of t x]
+by(auto simp: upd_list_simps upd_list_Cons upd_list_snoc neq_Leaf_iff split: tree.split)
+
+
+subsubsection "Proofs for delete"
+
+(* more del_simp lemmas; unify with basic set? *)
+
+lemma del_list_notin_Cons: "sorted (x # map fst xs) \<Longrightarrow> del_list x xs = xs"
+by(induction xs)(auto simp: sorted_Cons_iff)
+
+lemma del_list_sorted_app:
+  "sorted(map fst xs @ [x]) \<Longrightarrow> del_list x (xs @ ys) = xs @ del_list x ys"
+by (induction xs) (auto simp: sorted_mid_iff2)
+
+lemma inorder_splay_maxD:
+  "splay_max t = Node l a r \<Longrightarrow> sorted1(inorder t) \<Longrightarrow>
+  inorder l @ [a] = inorder t \<and> r = Leaf"
+by(induction t arbitrary: l a r rule: splay_max.induct)
+  (auto simp: sorted_lems splay_max_Leaf_iff split: tree.splits if_splits)
+
+lemma inorder_delete:
+  "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
+using inorder_splay[of x t, symmetric] sorted_splay[of t x]
+by (auto simp: del_list_simps del_list_sorted_app delete_def
+  del_list_notin_Cons inorder_splay_maxD splay_Leaf_iff splay_max_Leaf_iff
+  split: tree.splits)
+
+
+subsubsection "Overall Correctness"
+
+interpretation Map_by_Ordered
+where empty = Leaf and lookup = lookup and update = update
+and delete = delete and inorder = inorder and wf = "\<lambda>_. True"
+proof (standard, goal_cases)
+  case 2 thus ?case by(simp add: lookup_eq)
+next
+  case 3 thus ?case by(simp add: inorder_update del: update.simps)
+next
+  case 4 thus ?case by(simp add: inorder_delete)
+qed auto
+
+end
diff -r ab2e862263e7 -r e3984606b4b6 src/HOL/Data_Structures/Splay_Set.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Splay_Set.thy	Mon Nov 02 11:56:38 2015 +0100
@@ -0,0 +1,209 @@
+(*
+Author: Tobias Nipkow
+Function defs follows AFP entry Splay_Tree, proofs are new.
+*)
+
+section "Splay Tree Implementation of Sets"
+
+theory Splay_Set
+imports
+  "~~/src/HOL/Library/Tree"
+  Set_by_Ordered
+begin
+
+function splay :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+"splay a Leaf = Leaf" |
+"splay a (Node t1 a t2) = Node t1 a t2" |
+"a<b \<Longrightarrow> splay a (Node (Node t1 a t2) b t3) = Node t1 a (Node t2 b t3)" |
+"x<a \<Longrightarrow> splay x (Node Leaf a t) = Node Leaf a t" |
+"x<a \<Longrightarrow> x<b \<Longrightarrow> splay x (Node (Node Leaf a t1) b t2) = Node Leaf a (Node t1 b t2)" |
+"x<a \<Longrightarrow> x<b \<Longrightarrow> t1 \<noteq> Leaf \<Longrightarrow>
+ splay x (Node (Node t1 a t2) b t3) =
+ (case splay x t1 of Node t11 y t12 \<Rightarrow> Node t11 y (Node t12 a (Node t2 b t3)))" |
+"a<x \<Longrightarrow> x<b \<Longrightarrow> splay x (Node (Node t1 a Leaf) b t2) = Node t1 a (Node Leaf b t2)" |
+"a<x \<Longrightarrow> x<b \<Longrightarrow> t2 \<noteq> Leaf \<Longrightarrow>
+ splay x (Node (Node t1 a t2) b t3) =
+ (case splay x t2 of Node t21 y t22 \<Rightarrow> Node (Node t1 a t21) y (Node t22 b t3))" |
+"a<b \<Longrightarrow> splay b (Node t1 a (Node t2 b t3)) = Node (Node t1 a t2) b t3" |
+"a<x \<Longrightarrow> splay x (Node t a Leaf) = Node t a Leaf" |
+"a<x \<Longrightarrow> x<b \<Longrightarrow>  t2 \<noteq> Leaf \<Longrightarrow>
+ splay x (Node t1 a (Node t2 b t3)) =
+ (case splay x t2 of Node t21 y t22 \<Rightarrow> Node (Node t1 a t21) y (Node t22 b t3))" |
+"a<x \<Longrightarrow> x<b \<Longrightarrow> splay x (Node t1 a (Node Leaf b t2)) = Node (Node t1 a Leaf) b t2" |
+"a<x \<Longrightarrow> b<x \<Longrightarrow> splay x (Node t1 a (Node t2 b Leaf)) = Node (Node t1 a t2) b Leaf" |
+"a<x \<Longrightarrow> b<x \<Longrightarrow>  t3 \<noteq> Leaf \<Longrightarrow>
+ splay x (Node t1 a (Node t2 b t3)) =
+ (case splay x t3 of Node t31 y t32 \<Rightarrow> Node (Node (Node t1 a t2) b t31) y t32)"
+apply(atomize_elim)
+apply(auto)
+(* 1 subgoal *)
+apply (subst (asm) neq_Leaf_iff)
+apply(auto)
+apply (metis tree.exhaust less_linear)+
+done
+
+termination splay
+by lexicographic_order
+
+lemma splay_code: "splay x t = (case t of Leaf \<Rightarrow> Leaf |
+  Node al a ar \<Rightarrow>
+  (if x=a then t else
+   if x < a then
+     case al of
+       Leaf \<Rightarrow> t |
+       Node bl b br \<Rightarrow>
+         (if x=b then Node bl b (Node br a ar) else
+          if x < b then
+            if bl = Leaf then Node bl b (Node br a ar)
+            else case splay x bl of
+                   Node bll y blr \<Rightarrow> Node bll y (Node blr b (Node br a ar))
+          else
+          if br = Leaf then Node bl b (Node br a ar)
+          else case splay x br of
+                 Node brl y brr \<Rightarrow> Node (Node bl b brl) y (Node brr a ar))
+   else
+   case ar of
+     Leaf \<Rightarrow> t |
+     Node bl b br \<Rightarrow>
+       (if x=b then Node (Node al a bl) b br else
+        if x < b then
+          if bl = Leaf then Node (Node al a bl) b br
+          else case splay x bl of
+                 Node bll y blr \<Rightarrow> Node (Node al a bll) y (Node blr b br)
+        else if br=Leaf then Node (Node al a bl) b br
+             else case splay x br of
+                    Node bll y blr \<Rightarrow> Node (Node (Node al a bl) b bll) y blr)))"
+by(auto split: tree.split)
+
+definition is_root :: "'a \<Rightarrow> 'a tree \<Rightarrow> bool" where
+"is_root a t = (case t of Leaf \<Rightarrow> False | Node _ x _ \<Rightarrow> x = a)"
+
+definition "isin t x = is_root x (splay x t)"
+
+hide_const (open) insert
+
+fun insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+"insert x t =  (if t = Leaf then Node Leaf x Leaf
+  else case splay x t of
+    Node l a r \<Rightarrow> if x = a then Node l a r
+      else if x < a then Node l x (Node Leaf a r) else Node (Node l a Leaf) x r)"
+
+
+fun splay_max :: "'a tree \<Rightarrow> 'a tree" where
+"splay_max Leaf = Leaf" |
+"splay_max (Node l b Leaf) = Node l b Leaf" |
+"splay_max (Node l b (Node rl c rr)) =
+  (if rr = Leaf then Node (Node l b rl) c Leaf
+   else case splay_max rr of
+     Node rrl m rrr \<Rightarrow> Node (Node (Node l b rl) c rrl) m rrr)"
+
+
+definition delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+"delete x t = (if t = Leaf then Leaf
+  else case splay x t of Node l a r \<Rightarrow>
+    if x = a
+    then if l = Leaf then r else case splay_max l of Node l' m r' \<Rightarrow> Node l' m r
+    else Node l a r)"
+
+
+subsection "Functional Correctness Proofs"
+
+lemma splay_Leaf_iff: "(splay a t = Leaf) = (t = Leaf)"
+by(induction a t rule: splay.induct) (auto split: tree.splits)
+
+lemma splay_max_Leaf_iff: "(splay_max t = Leaf) = (t = Leaf)"
+by(induction t rule: splay_max.induct)(auto split: tree.splits)
+
+
+subsubsection "Proofs for isin"
+
+lemma
+  "splay x t = Node l a r \<Longrightarrow> sorted(inorder t) \<Longrightarrow>
+  x \<in> elems (inorder t) \<longleftrightarrow> x=a"
+by(induction x t arbitrary: l a r rule: splay.induct)
+  (auto simp: elems_simps1 splay_Leaf_iff ball_Un split: tree.splits)
+
+lemma splay_elemsD:
+  "splay x t = Node l a r \<Longrightarrow> sorted(inorder t) \<Longrightarrow>
+  x \<in> elems (inorder t) \<longleftrightarrow> x=a"
+by(induction x t arbitrary: l a r rule: splay.induct)
+  (auto simp: elems_simps2 splay_Leaf_iff split: tree.splits)
+
+lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
+by (auto simp: isin_def is_root_def splay_elemsD splay_Leaf_iff split: tree.splits)
+
+
+subsubsection "Proofs for insert"
+
+(* more sorted lemmas; unify with basic set? *)
+
+lemma sorted_snoc_le:
+  "ASSUMPTION(sorted(xs @ [x])) \<Longrightarrow> x \<le> y \<Longrightarrow> sorted (xs @ [y])"
+by (auto simp add: Sorted_Less.sorted_snoc_iff ASSUMPTION_def)
+
+lemma sorted_Cons_le:
+  "ASSUMPTION(sorted(x # xs)) \<Longrightarrow> y \<le> x \<Longrightarrow> sorted (y # xs)"
+by (auto simp add: Sorted_Less.sorted_Cons_iff ASSUMPTION_def)
+
+lemma inorder_splay: "inorder(splay x t) = inorder t"
+by(induction x t rule: splay.induct)
+  (auto simp: neq_Leaf_iff split: tree.split)
+
+lemma sorted_splay:
+  "sorted(inorder t) \<Longrightarrow> splay x t = Node l a r \<Longrightarrow>
+  sorted(inorder l @ x # inorder r)"
+unfolding inorder_splay[of x t, symmetric]
+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)
+
+lemma ins_list_Cons: "sorted (x # xs) \<Longrightarrow> ins_list x xs = x # xs"
+by (induction xs) auto
+
+lemma ins_list_snoc: "sorted (xs @ [x]) \<Longrightarrow> ins_list x xs = xs @ [x]"
+by(induction xs) (auto simp add: sorted_mid_iff2)
+
+lemma inorder_insert:
+  "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
+using inorder_splay[of x t, symmetric] sorted_splay[of t x]
+by(auto simp: ins_list_simps ins_list_Cons ins_list_snoc neq_Leaf_iff split: tree.split)
+
+
+subsubsection "Proofs for delete"
+
+(* more del_simp lemmas; unify with basic set? *)
+
+lemma del_list_notin_Cons: "sorted (x # xs) \<Longrightarrow> del_list x xs = xs"
+by(induction xs)(auto simp: sorted_Cons_iff)
+
+lemma del_list_sorted_app:
+  "sorted(xs @ [x]) \<Longrightarrow> del_list x (xs @ ys) = xs @ del_list x ys"
+by (induction xs) (auto simp: sorted_mid_iff2)
+
+lemma inorder_splay_maxD:
+  "splay_max t = Node l a r \<Longrightarrow> sorted(inorder t) \<Longrightarrow>
+  inorder l @ [a] = inorder t \<and> r = Leaf"
+by(induction t arbitrary: l a r rule: splay_max.induct)
+  (auto simp: sorted_lems splay_max_Leaf_iff split: tree.splits if_splits)
+
+lemma inorder_delete:
+  "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
+using inorder_splay[of x t, symmetric] sorted_splay[of t x]
+by (auto simp: del_list_simps del_list_sorted_app delete_def
+  del_list_notin_Cons inorder_splay_maxD splay_Leaf_iff splay_max_Leaf_iff
+  split: tree.splits)
+
+
+subsubsection "Overall Correctness"
+
+interpretation Set_by_Ordered
+where empty = Leaf and isin = isin and insert = insert
+and delete = delete and inorder = inorder and wf = "\<lambda>_. True"
+proof (standard, goal_cases)
+  case 2 thus ?case by(simp add: isin_set)
+next
+  case 3 thus ?case by(simp add: inorder_insert del: insert.simps)
+next
+  case 4 thus ?case by(simp add: inorder_delete)
+qed auto
+
+end
diff -r ab2e862263e7 -r e3984606b4b6 src/HOL/Data_Structures/document/root.bib
--- a/src/HOL/Data_Structures/document/root.bib	Mon Nov 02 11:56:28 2015 +0100
+++ b/src/HOL/Data_Structures/document/root.bib	Mon Nov 02 11:56:38 2015 +0100
@@ -6,3 +6,10 @@
 
 @book{Okasaki,author={Chris Okasaki},title="Purely Functional Data Structures",
 publisher="Cambridge University Press",year=1998}
+
+@article{Schoenmakers-IPL93,author="Berry Schoenmakers",
+title="A Systematic Analysis of Splaying",journal={Information Processing Letters},volume=45,pages={41-50},year=1993}
+
+@article{SleatorT-JACM85,author={Daniel D. Sleator and Robert E. Tarjan},
+title={Self-adjusting Binary Search Trees},journal={J. ACM},
+volume=32,number=3,pages={652-686},year=1985}
diff -r ab2e862263e7 -r e3984606b4b6 src/HOL/Data_Structures/document/root.tex
--- a/src/HOL/Data_Structures/document/root.tex	Mon Nov 02 11:56:28 2015 +0100
+++ b/src/HOL/Data_Structures/document/root.tex	Mon Nov 02 11:56:38 2015 +0100
@@ -44,6 +44,10 @@
 \paragraph{2-3 trees}
 The function definitions are based on the teaching material by Franklyn Turbak.
 
+\paragraph{Splay trees}
+They were invented by Sleator and Tarjan \cite{SleatorT-JACM85}.
+Our formalisation follows Schoenmakers \cite{Schoenmakers-IPL93}.
+
 \bibliographystyle{abbrv}
 \bibliography{root}
 
diff -r ab2e862263e7 -r e3984606b4b6 src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Nov 02 11:56:28 2015 +0100
+++ b/src/HOL/ROOT	Mon Nov 02 11:56:38 2015 +0100
@@ -174,12 +174,12 @@
   theories [document = false]
     "Less_False"
   theories
-    Tree_Set
     Tree_Map
     AVL_Map
     RBT_Map
     Tree23_Map
     Tree234_Map
+    Splay_Map
   document_files "root.tex" "root.bib"
 
 session "HOL-Import" in Import = HOL +
diff -r ab2e862263e7 -r e3984606b4b6 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Mon Nov 02 11:56:28 2015 +0100
+++ b/src/Pure/GUI/gui.scala	Mon Nov 02 11:56:38 2015 +0100
@@ -34,8 +34,7 @@
       if (Platform.is_windows || Platform.is_macos)
         UIManager.getSystemLookAndFeelClassName()
       else
-        find_laf("Nimbus") getOrElse
-          UIManager.getCrossPlatformLookAndFeelClassName()
+        UIManager.getCrossPlatformLookAndFeelClassName()
     }
 
   def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
diff -r ab2e862263e7 -r e3984606b4b6 src/Pure/General/time.scala
--- a/src/Pure/General/time.scala	Mon Nov 02 11:56:28 2015 +0100
+++ b/src/Pure/General/time.scala	Mon Nov 02 11:56:38 2015 +0100
@@ -15,8 +15,10 @@
 {
   def seconds(s: Double): Time = new Time((s * 1000.0).round)
   def ms(m: Long): Time = new Time(m)
+  def now(): Time = ms(System.currentTimeMillis())
+
   val zero: Time = ms(0)
-  def now(): Time = ms(System.currentTimeMillis())
+  val start: Time = now()
 
   def print_seconds(s: Double): String =
     String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
diff -r ab2e862263e7 -r e3984606b4b6 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Nov 02 11:56:28 2015 +0100
+++ b/src/Pure/Isar/attrib.ML	Mon Nov 02 11:56:38 2015 +0100
@@ -510,7 +510,7 @@
 (* theory setup *)
 
 val _ = Theory.setup
- (register_config quick_and_dirty_raw #>
+ (register_config Goal.quick_and_dirty_raw #>
   register_config Ast.trace_raw #>
   register_config Ast.stats_raw #>
   register_config Printer.show_brackets_raw #>
diff -r ab2e862263e7 -r e3984606b4b6 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Mon Nov 02 11:56:28 2015 +0100
+++ b/src/Pure/goal.ML	Mon Nov 02 11:56:38 2015 +0100
@@ -6,6 +6,7 @@
 
 signature BASIC_GOAL =
 sig
+  val quick_and_dirty: bool Config.T
   val parallel_proofs: int Unsynchronized.ref
   val SELECT_GOAL: tactic -> int -> tactic
   val PREFER_GOAL: tactic -> int -> tactic
@@ -38,6 +39,7 @@
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val prove_global: theory -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
+  val quick_and_dirty_raw: Config.raw
   val prove_sorry: Proof.context -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val prove_sorry_global: theory -> string list -> term list -> term ->
@@ -250,6 +252,12 @@
 fun prove_global thy xs asms prop tac =
   Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);
 
+
+(* skip proofs *)
+
+val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", @{here});
+val quick_and_dirty = Config.bool quick_and_dirty_raw;
+
 fun prove_sorry ctxt xs asms prop tac =
   if Config.get ctxt quick_and_dirty then
     prove ctxt xs asms prop (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt))
diff -r ab2e862263e7 -r e3984606b4b6 src/Pure/skip_proof.ML
--- a/src/Pure/skip_proof.ML	Mon Nov 02 11:56:28 2015 +0100
+++ b/src/Pure/skip_proof.ML	Mon Nov 02 11:56:38 2015 +0100
@@ -4,9 +4,6 @@
 Skip proof via oracle invocation.
 *)
 
-val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", @{here});
-val quick_and_dirty = Config.bool quick_and_dirty_raw;
-
 signature SKIP_PROOF =
 sig
   val report: Proof.context -> unit
diff -r ab2e862263e7 -r e3984606b4b6 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Mon Nov 02 11:56:28 2015 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Mon Nov 02 11:56:38 2015 +0100
@@ -1,5 +1,4 @@
 #jEdit properties
-action-bar.shortcut=C+ENTER
 buffer.deepIndent=false
 buffer.encoding=UTF-8-Isabelle
 buffer.indentSize=2
@@ -241,7 +240,7 @@
 line-end.shortcut=END
 line-home.shortcut=HOME
 logo.icon.medium=32x32/apps/isabelle.gif
-lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel
+lookAndFeel=javax.swing.plaf.metal.MetalLookAndFeel
 match-bracket.shortcut2=C+9
 navigator.showOnToolbar=true
 next-bracket.shortcut2=C+e C+9