.

Binary file Exercises/exam.pdf has changed

--- a/Exercises/exam/Q_Balanced_Insert.thy	Tue Jul 25 11:29:03 2017 +0200
+++ b/Exercises/exam/Q_Balanced_Insert.thy	Wed Jul 26 16:40:05 2017 +0200
@@ -17,7 +17,7 @@
     Recall the standard insertion function for unbalanced binary search trees.
     @{thm [display] ins.simps}
     We want to insert the elements of a list into a search tree:
-    @{thm from_list_def}
+    @{thm from_list_def}.
     Your task is to specify a function that preprocesses the list, 
     such that the resulting tree is balanced. You may assume the list
     is sorted, distinct, and has exactly \<open>2^k - 1\<close> elements for some \<open>k\<close>.

--- a/ROOT	Tue Jul 25 11:29:03 2017 +0200
+++ b/ROOT	Wed Jul 26 16:40:05 2017 +0200
@@ -62,3 +62,24 @@
   document_files
     "root_amor.tex"
     "prelude.tex"
+
+session MOD_Slides in Slides = "HOL-FDS17" +
+  options [document_output = tex, document = pdf, names_short = true,
+           document_variants = "mod"]
+  theories[show_question_marks=false]
+    MOD_Intro_Slides
+    Time_Slides
+(*    Tree_Slides*)
+    Search_Trees
+    Tree23_Slides
+    RBT_Slides
+    Leftist_Heap_Slides
+    Braun_Tree_Slides
+    Binomial_Tree_Slides
+    Amor_Slides
+    Skew_Heap_Slides
+    Splay_Tree_Slides
+    Pairing_Heap_Slides
+  document_files
+    "root_mod.tex"
+    "prelude.tex"

--- a/Slides/Sorting_Slides.thy	Tue Jul 25 11:29:03 2017 +0200
+++ b/Slides/Sorting_Slides.thy	Wed Jul 26 16:40:05 2017 +0200
@@ -5,11 +5,6 @@
   "../../Public/Thys/Sorting"
 begin
 
-definition dummyid :: "'a \<Rightarrow> 'a" where
-"dummyid x = x"
-
-notation (latex output) dummyid ("_")
-
 lemma sorted_Cons: "sorted (x # xs) = ((\<forall>y\<in>set xs. x \<le> dummyid y) & sorted xs)"
 by(simp add: dummyid_def)