summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Wed, 26 Jul 2017 16:40:05 +0200 | |

changeset 69869 | 0bba9c6b2a17 |

parent 69868 | 00f70c27c44b |

child 69871 | 9e9c2bba0e05 |

.

--- 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)