author lammich Sat, 29 Jul 2017 19:35:49 +0200 changeset 69876 295b5feb4e9c parent 69875 dff3ec88324d (current diff) parent 69871 9e9c2bba0e05 (diff) child 69877 3a4da8caad49 child 69879 3829e486b17a
merged
 Exercises/exam.pdf file | annotate | diff | comparison | revisions Exercises/exam/Q_Balanced_Insert.thy file | annotate | diff | comparison | revisions
```--- a/ROOT	Sat Jul 29 19:34:29 2017 +0200
+++ b/ROOT	Sat Jul 29 19:35:49 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	Sat Jul 29 19:34:29 2017 +0200
+++ b/Slides/Sorting_Slides.thy	Sat Jul 29 19:35:49 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)"