--- 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)"
by(simp add: dummyid_def)