merged draft
authornipkow
Thu, 03 Aug 2017 09:43:22 +0200
changeset 69889 cbd6b89c79e1
parent 69888 95658663e63d (current diff)
parent 69885 dbd3e3d7657d (diff)
child 69890 eef3c9ef1c3e
merged
--- a/Slides/Binomial_Tree_Slides.thy	Wed Aug 02 17:48:54 2017 +0200
+++ b/Slides/Binomial_Tree_Slides.thy	Thu Aug 03 09:43:22 2017 +0200
@@ -23,23 +23,29 @@
 %-------------------------------------------------------------
 \section{Binomial Heaps}
 %-------------------------------------------------------------
-\thyfile{Thys/BinHeap}{Binomial Heaps --- Correctness and Complexity}
+\ifMOD\else\thyfile{Thys/BinHeap}{Binomial Heaps --- Correctness and Complexity}\fi
 %-------------------------------------------------------------
+\begin{frame}{Numerical method}
+Idea: only use trees \<open>t\<^sub>i\<close> of size \<open>2\<^sup>i\<close>\\
+\pause
 
-\begin{frame}{Numerical Method}{See \emph{Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1999}}
-  Only use trees \<open>t\<^sub>i\<close> of size \<open>2\<^sup>i\<close>\\
-  \smallskip\pause
+\begin{example}
+To store (in binary) \<open>11001\<close> elements: \<open>[t\<^sub>0,0,0,t\<^sub>3,t\<^sub>4]\<close>\\
+\end{example}
+\pause
 
-  E.g., to store \<open>0b11001\<close> elements: \<open>[t\<^sub>0,0,0,t\<^sub>3,t\<^sub>4]\<close>\\
-  \smallskip\pause
+Merge $\approx$ addition with carry
+\pause
 
-  Meld: Addition with carry. \\
-  \smallskip\pause
-  Linking two trees of size \<open>2\<^sup>i\<close>: Yields size \<open>2\<^sup>i\<^sup>+\<^sup>1\<close> \\
+Needs function to combine
+\begin{tabular}[t]{l}
+two trees of size \<open>2\<^sup>i\<close>\\
+into one tree of size \<open>2\<^sup>i\<^sup>+\<^sup>1\<close>
+\end{tabular}
 \end{frame}
-
-\begin{frame}{Organization of Trees}
-  \high{@{theory_text \<open>(*<*)datatype (*>*)'a tree = Node (rank: nat) (root: 'a) (children: "'a tree list")\<close>}}\\
+%-------------------------------------------------------------
+\begin{frame}{Binomial trees}
+\high{@{theory_text \<open>datatype 'a tree = Node (rank: nat) (root: 'a) ("'a tree list")\<close>}}\\
   \smallskip\pause
   
   Node with rank \<open>i\<close> has successors \<open>[t\<^sub>i\<^sub>-\<^sub>1,\<dots>t\<^sub>0]\<close>
@@ -50,7 +56,7 @@
   Tree has exactly @{term \<open>(2::nat)^rank t\<close>} nodes
   \high{@{thm [display] size_btree}}
 \end{frame}
-
+%-------------------------------------------------------------
 \begin{frame}{Linking two Trees}
   Given two trees of rank \<open>i\<close>, join them to tree of rank \<open>i+1\<close>.\\
   \smallskip\pause
@@ -60,7 +66,7 @@
 
   \high{@{thm[display] link_def}}
 \end{frame}
-
+%-------------------------------------------------------------
 \begin{frame}{Heap Datatype}
   Using sparse representation for binary numbers: \\
   \<open>[t\<^sub>0,0,0,t\<^sub>3,t\<^sub>4]\<close> represented as \<open>[ (0,t\<^sub>0), (3,t\<^sub>3),(4,t\<^sub>4) ]\<close>
@@ -72,7 +78,7 @@
   \high{@{thm bheap_invar_def}}\\
   Ranks in \high{ascending} order\\
 \end{frame}
-
+%-------------------------------------------------------------
 \begin{frame}{Inserting a Tree}
   \high{@{thm [display, margin=60] ins_tree.simps}}
   \smallskip\pause
@@ -83,7 +89,7 @@
   Precondition:\\
   Rank of inserted tree \<open>\<le>\<close> ranks of trees in heap \\
 \end{frame}
-
+%-------------------------------------------------------------
 \begin{frame}{Merge}
   \high{@{thm [display] merge_simps}}
   \smallskip\pause
@@ -93,7 +99,7 @@
 
   Note: Handling of carry after recursive call
 \end{frame}
-
+%-------------------------------------------------------------
 \begin{frame}{Find/Delete Minimum Element}
   All trees are min-heaps
   \smallskip\pause
@@ -111,7 +117,7 @@
   Note the \<open>rev\<close>!
 
 \end{frame}
-
+%-------------------------------------------------------------
 \begin{frame}{Complexity}
   Recall: @{term \<open>size (mset_tree t) = 2^rank t\<close>}
   \smallskip\pause
@@ -125,7 +131,7 @@
 
   Proofs: \pause straightforward\pause ?
 \end{frame}
-
+%-------------------------------------------------------------
 \begin{frame}{Complexity of Merge}
   \high{@{thm [display] merge_simps(3)}}
   \smallskip\pause
@@ -138,7 +144,7 @@
 
   Yields (roughly) \<open>m n = m (n-2) + n\<close> \pause quadratic!
 \end{frame}
-
+%-------------------------------------------------------------
 \begin{frame}{Complexity of Merge}
   \high{@{thm [display] merge_simps(3)}}
   \smallskip\pause
--- a/Slides/Braun_Tree_Slides.thy	Wed Aug 02 17:48:54 2017 +0200
+++ b/Slides/Braun_Tree_Slides.thy	Thu Aug 03 09:43:22 2017 +0200
@@ -4,8 +4,31 @@
   Tree_Notation
   "$AFP/Priority_Queue_Braun/Priority_Queue_Braun"
 begin
+
+fun sm :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> bool" where
+"sm Leaf Leaf = True" |
+"sm (Node l _ r) (Node l' _ r') = (sm l l' \<and> sm r r')" |
+"sm _ _ = False"
+
+lemma "braun t \<Longrightarrow> braun t' \<Longrightarrow> size t = size t' \<Longrightarrow> sm t t'"
+apply(induction t arbitrary: t')
+ apply (simp add: size_0_iff_Leaf)
+apply(case_tac t')
+ apply simp
+apply auto
+done
+
 notation (output) insert_pq ("insert")
 
+(* FIXME +1 in AFP source *)
+lemma braun_simp2: "braun (Node l x r) = (size r \<le> size l \<and> size l \<le> size r + 1 \<and> braun l \<and> braun r)"
+by simp
+lemmas braun_simps = braun.simps(1) braun_simp2
+
+lemma del_left_simp2:
+  "l \<noteq> Leaf \<Longrightarrow> del_left (Node l x r) = (let (y,l') = del_left l in (y,Node r x l'))"
+by (auto simp: neq_Leaf_iff)
+
 lemma del_min_simp3: "l \<noteq> Leaf \<Longrightarrow>
   del_min (Node l x r) = (let (y,l') = del_left l in sift_down r y l')"
 by(auto simp: neq_Leaf_iff)
@@ -18,29 +41,58 @@
 %-------------------------------------------------------------
 \afpentry{Priority_Queue_Braun}
 %-------------------------------------------------------------
+\ifMOD
+\begin{frame}
+Based on code from\smallskip\\
+L.C. Paulson. \emph{ML for the Working Programmer}. 1996
+\smallskip\pause
+
+based on code from Chris Okasaki.
+\end{frame}
+\fi
+%-------------------------------------------------------------
+\tikzset{hide on/.code={\only<#1>{\color{white}}}}
 \begin{frame}{What is a Braun tree?}
 @{const_typ braun}\\\smallskip\pause
-\high{@{thm[break,margin=60] braun.simps}}\\
-\bigskip\pause
+\high{@{thm[break,margin=60] braun_simps}}\\
+\pause
+\begin{center}
+\begin{tikzpicture}
+  [thick,level 1/.style={sibling distance=20mm},level 2/.style={sibling distance=10mm}]
+  \node {1}
+    child[hide on=-3] {node {2}
+      child[hide on=-5] {node {4}}
+      child[hide on=-7] {node {6}}
+    }
+    child[hide on=-4] {node {3}
+      child[hide on=-6] {node {5}}
+      child[hide on=-8] {node {7}}
+    };
+\end{tikzpicture}
+\end{center}
+\onslide<10>
 
 \textbf{Lemma} \high{@{thm height_size_braun}}
 \end{frame}
 %-------------------------------------------------------------
-\begin{frame}{Idea of Invariant Maintenance}
-\high{@{thm[break,margin=60] braun.simps}}
+\begin{frame}{Idea of invariant maintenance}
+\high{@{thm[break,margin=60] braun_simps}}
 \bigskip\pause
 
-Add element: \pause to right subtree, then swap subtrees\\ \pause
-  {\bf Goal}: @{term "size l \<le> size r + 1 \<and> size r + 1 \<le> size l + 1"} \pause\qed
-
+Add element: \pause to right subtree, then swap subtrees\\
+\ifMOD\else\pause
+\textbf{Goal}: @{prop "size (l::'a tree) \<le> size (r::'a tree) + 1 \<and> size r + 1 \<le> size l + 1"} \pause\qed
+\fi
 \bigskip\pause
-Remove element: \pause from left subtree, then swap subtrees\\ \pause
- {\bf Goal}: @{term "size l - 1 \<le> size r \<and> size r \<le> size l"} \pause\qed
 
+Remove element: \pause from left subtree, then swap subtrees\\
+\ifMOD\else\pause
+\textbf{Goal}: @{prop "size (l::'a tree) - 1 \<le> size (r::'a tree) \<and> size r \<le> size l"} \pause\qed
+\fi
 \end{frame}
 %-------------------------------------------------------------
 \begin{frame}{Priority queue implementation}
-Implementation type: ordinary binary trees
+Implementation type: @{typ "'a tree"}
 \bigskip\pause
 
 Invariants: @{const heap} and @{const braun}
@@ -63,30 +115,44 @@
 @{const_typ del_min}\\\smallskip\pause
 \high{@{thm [break,margin=60] (concl) del_min_simps}}
 \bigskip\pause
-
-Idea: Delete leftmost element $y$, put it at top, and sift it down
-  to adequate position.
+\begin{enumerate}
+\item Delete leftmost element $y$
+\item Sift $y$ from the root down
+\end{enumerate}
 \end{frame}
 %-------------------------------------------------------------
 \begin{frame}{@{const del_left}}
 \high<1>{@{const_typ del_left}}\\\smallskip\pause
-\high<2>{@{thm [break,margin=60] (sub) del_left.simps(1)}}\\\smallskip\pause
-\high<3>{@{thm [break,margin=60] (sub) del_left.simps(2)}}
+\high<2>{@{thm [break,margin=60] del_left.simps(1)}}\\\smallskip\pause
+\high<3>{@{thm [break,margin=60] (concl) del_left_simp2}}
 \end{frame}
 %-------------------------------------------------------------
 \begin{frame}{@{const sift_down}}
 \high<1>{@{const_typ sift_down}}\\\smallskip\pause
+\ifMOD
+\high<2-3>{@{text "sift_down (t\<^sub>1 = (Node l\<^sub>1 x\<^sub>1 r\<^sub>1)) a (t\<^sub>2 = (Node l\<^sub>2 x\<^sub>2 r\<^sub>2))"}}\\
+\high<2-3>{\<open>=\<close>}\\\pause
+\high<3>{@{term[break,margin=60] (sub) "(if a \<le> x1 \<and> a \<le> x2
+   then Node t1 a t2
+   else if x1 \<le> x2 then Node (sift_down l1 a r1) x1 t2
+        else Node t1 x2 (sift_down l2 a r2))"}}
+\else
 \high<2>{@{thm [break,margin=60] (sub) sift_down.simps(1)}}\\\smallskip\pause
 \high<3>{@{thm [break,margin=60] (sub) sift_down.simps(2)}}\\\smallskip\pause
-\high<4>{@{thm [break,margin=60] (sub) sift_down.simps(3)}}
+%\high<4>{@ {thm [break,margin=60] (sub) sift_down.simps(3)}}
+\high<4-5>{@{text "sift_down (t\<^sub>1 = (Node l\<^sub>1 x\<^sub>1 r\<^sub>1)) a (t\<^sub>2 = (Node l\<^sub>2 x\<^sub>2 r\<^sub>2))"}}\\
+\high<4-5>{\<open>=\<close>}\\\pause
+\high<5>{@{term[break,margin=60] (sub) "(if a \<le> x1 \<and> a \<le> x2
+   then Node t1 a t2
+   else if x1 \<le> x2 then Node (sift_down l1 a r1) x1 t2
+        else Node t1 x2 (sift_down l2 a r2))"}}
 \bigskip\pause
 
-Maintenance of @{const braun}: Preserves structure of tree.
+Maintains @{const braun}
+\fi
 \end{frame}
-
-
 %-------------------------------------------------------------
-\begin{frame}{Functional correctness proofs for deletion}
+\begin{frame}{Functional correctness proofs for @{const del_min}}
 Many lemmas, mostly straightforward
 \end{frame}
 %-------------------------------------------------------------
@@ -104,6 +170,7 @@
 Above running times logarithmic in size
 \end{frame}
 %-------------------------------------------------------------
+\ifMOD\else
 \begin{frame}[t]{Sorting with priority queue}
 \pause
 
@@ -123,7 +190,7 @@
 
 %Braun trees $\leadsto$ functional version of heap sort
 \end{frame}
-
+\fi
 %%-------------------------------------------------------------
 %\begin{frame}[t]{Sorting with priority queue}
 %
--- a/Slides/Leftist_Heap_Slides.thy	Wed Aug 02 17:48:54 2017 +0200
+++ b/Slides/Leftist_Heap_Slides.thy	Thu Aug 03 09:43:22 2017 +0200
@@ -14,6 +14,25 @@
 \end{isabellebody}%
 \section{Priority Queues}
 %-------------------------------------------------------------
+\ifMOD
+\begin{frame}{Priority queue informally}
+\begin{center}
+Collection of elements with priorities
+\bigskip\pause
+
+We focus on the priorities:\\
+\high{element = priority}
+\bigskip\pause
+
+The same element can be contained \high{multiple times}\\ in a priority queue
+\pause
+
+$\Longrightarrow$
+
+The abstract view of a priority queue is a \high{multiset}
+\end{center}
+\end{frame}
+\else
 \begin{frame}{Priority queue informally}
 \begin{center}
 Collection of elements with priorities
@@ -49,11 +68,7 @@
 The abstract view of a priority queue is a \high{multiset}
 \end{center}
 \end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Multisets in Isabelle}
-
-Import \texttt{"Library/Multiset"}
-\end{frame}
+\fi
 %-------------------------------------------------------------
 *}
 text_raw (in Priority_Queue) {*
@@ -68,15 +83,15 @@
 \pause
 \item An implementation type \ \high{@{typ 'q}}
 \pause
-\item \high{\<open>empty ::\<close> @{typ 'q}}
+\item<-8> \high{\<open>empty ::\<close> @{typ 'q}}
 \pause
-\item \high{\<open>is_empty ::\<close> @{typ "'q \<Rightarrow> bool"}}
+\item<-8> \high{\<open>is_empty ::\<close> @{typ "'q \<Rightarrow> bool"}}
 \pause
-\item \high{\<open>insert ::\<close> @{typ"'a \<Rightarrow> 'q \<Rightarrow> 'q"}}
+\item<-9> \high{\<open>insert ::\<close> @{typ"'a \<Rightarrow> 'q \<Rightarrow> 'q"}}
 \pause
-\item \high{\<open>get_min ::\<close> @{typ"'q \<Rightarrow> 'a"}}
+\item<-8> \high{\<open>get_min ::\<close> @{typ"'q \<Rightarrow> 'a"}}
 \pause
-\item \high{\<open>del_min ::\<close> @{typ"'q \<Rightarrow> 'q"}}
+\item<-9> \high{\high{\<open>del_min ::\<close> @{typ"'q \<Rightarrow> 'q"}}}
 \end{itemize}
 \end{frame}
 %-------------------------------------------------------------
@@ -103,25 +118,29 @@
 \end{frame}
 %-------------------------------------------------------------
 \begin{frame}{Correctness of implementation}
-Must prove \ \high{@{prop"invar q"}} \<open>\<Longrightarrow>\<close>\medskip
+Must prove \ \high{@{prop"invar q"} \<open>\<Longrightarrow>\<close>}\medskip
 
 \pause
+\ifMOD\else
 \high{@{thm mset_empty}}\smallskip\\\pause
 \high{@{thm (concl) is_empty}}\smallskip\\\pause
-\high{@{thm (concl) mset_insert}}\medskip\\\pause
-\high{@{thm (prem 2) get_min} \<open>\<Longrightarrow>\<close>}\\
-\high{@{thm (concl) mset_del_min}}\smallskip\\\pause
-\high{@{thm (concl) mset_get_min}}\\
+\fi
+\high{@{thm (concl) mset_insert}}\smallskip\\\pause
+\ifMOD\else
+\high{@{thm (prem 2) mset_get_min} \<open>\<Longrightarrow>\<close> @{thm (concl) mset_get_min}}\smallskip\\\pause
+\fi
+\high{@{thm (prem 2) mset_del_min} \<open>\<Longrightarrow>\<close>}\\
+\high{@{thm (concl) mset_del_min}}\\
 \bigskip\pause
-\high{@{thm (concl) invar_empty}}\\
+\ifMOD\else\high{@{thm (concl) invar_empty}}\\\fi
 \high{@{thm (concl) invar_insert}}\\
 \high{@{thm (concl) invar_del_min}}
 \end{frame}
 %-------------------------------------------------------------
 \begin{frame}{Terminology}
 \begin{center}
-A tree is a \high{heap} if for every subtree\\
-the root is $\le$ all elements in the subtrees.
+A tree is a \concept{heap} if for every subtree\\
+the root is $\le$ all elements in that subtree.
 \end{center}
 \pause
 
@@ -130,10 +149,12 @@
 %-------------------------------------------------------------
 \begin{frame}{Priority queue via heap}
 \begin{itemize}
+\ifMOD\else
 \pause
 \item \<open>empty = \<langle>\<rangle>\<close>
 \pause
 \item \<open>is_empty h = (h = \<langle>\<rangle>)\<close>
+\fi
 \pause
 \item \<open>get_min \<langle>_, a, _\<rangle> = a\<close>
 \pause
@@ -145,6 +166,7 @@
 \end{itemize}
 \end{frame}
 %-------------------------------------------------------------
+\ifMOD\else
 \begin{frame}{Priority queue via heap}
 A naive merge:
 \medskip\pause
@@ -159,26 +181,27 @@
 
 \bad{Challenge:} how to maintain some kind of balance
 \end{frame}
+\fi
 %-------------------------------------------------------------
 *}
 text_raw {*
 %-------------------------------------------------------------
 \section{Leftist Heap}
 %-------------------------------------------------------------
-\thyfile{Leftist\char`_Heap}{}
+\ifMOD\else\thyfile{Thys/Leftist\char`_Heap}{}\fi
 %-------------------------------------------------------------
 \begin{frame}{Leftist tree informally}
-The \high{rank} of a tree is the depth of the rightmost leaf.
+The \concept{rank} of a tree is the depth of the rightmost leaf.
 \pause\bigskip
 
-In a \high{leftist tree}, the rank of every left child is $\ge$
-the rank of its right sibling
+In a \concept{leftist tree}, the rank of every left child is $\ge$
+the rank of its right sibling.
 
 \pause\bigskip
-Insertions are done on the right. Thus rank bounds number of descends.
+Merge descends along the right spine.\\ Thus rank bounds number of steps.
 
 \pause\bigskip
-If rank of right child gets to large: swap with left child.
+If rank of right child gets too large: swap with left child.
 
 \end{frame}
 %-------------------------------------------------------------
@@ -196,13 +219,14 @@
 \high{@{thm[break,margin=50] (dummy_pats) mset_tree.simps(2)}}
 \end{frame}
 %-------------------------------------------------------------
+\ifMOD\else
 \begin{frame}{Heap}
 @{const heap} \<open>::\<close> @{typ "'a lheap \<Rightarrow> bool"}\\\smallskip\pause
 \high{@{thm heap.simps(1)}}\\
 \high{@{text"heap \<langle>_, l, a, r\<rangle> = (heap l \<and> heap r \<and>"}}\\
 \quad\high{@{text"(\<forall>x \<in># mset_tree l + mset_tree r. a \<le> x))"}}
-
 \end{frame}
+\fi
 %-------------------------------------------------------------
 \begin{frame}{Leftist tree}
 @{const rank} \<open>::\<close> @{typ "'a lheap \<Rightarrow> nat"}\\\smallskip\pause
@@ -224,16 +248,6 @@
 \end{center}
 \end{frame}
 %-------------------------------------------------------------
-\begin{frame}{Why leftist tree?}
-\pause
-
-\textbf{Lemma} \high{@{thm pow2_rank_size1}}
-\bigskip\pause
-
-\textbf{Lemma} Execution time of @{term "merge t\<^sub>1 t\<^sub>2"} is bounded by
-\mbox{@{term"rank t\<^sub>1 + rank t\<^sub>2"}}
-\end{frame}
-%-------------------------------------------------------------
 \begin{frame}{@{const merge}}
 Principle: descend on the right
 \smallskip\pause
@@ -247,6 +261,7 @@
 where @{thm (dummy_pats) rk.simps(2)}
 \end{frame}
 %-------------------------------------------------------------
+\ifMOD\else
 \begin{frame}{@{const merge}}
 @{thm[break] (sub,dummy_pats) merge.simps(3)}
 \bigskip\pause
@@ -256,11 +271,24 @@
 \onslide<3->{\revealbeamer{@{term"size t\<^sub>1 + size t\<^sub>2"}}}
 \onslide<2->{decreases with every recursive call.}}
 \end{frame}
+\fi
 %-------------------------------------------------------------
 \begin{frame}{Functional correctness proofs}{including preservation of \<open>invar\<close>}
 Straightforward
 \end{frame}
 %-------------------------------------------------------------
+\ifMOD
+\begin{frame}{Logarithmic complexity}
+\begin{lemma}
+\high{@{thm pow2_rank_size1}}
+\end{lemma}
+\bigskip\pause
+
+\begin{corollary}
+@{thm[break,margin=40] t_merge_log}
+\end{corollary}
+\end{frame}
+\else
 \begin{frame}{Logarithmic complexity}
 Correlation of rank and size:\\ 
   \textbf{Lemma} @{thm pow2_rank_size1}
@@ -273,14 +301,15 @@
 \textbf{Lemma} @{thm t_merge_rank}
 \pause
 
-\textbf{Lemma} @{thm[break,margin=40] t_merge_log}
+\textbf{Corollary} @{thm[break,margin=40] t_merge_log}
 \pause\bigskip
 
-\textbf{Lemma}\\ @{thm t_insert_log}
+\textbf{Corollary}\\ @{thm t_insert_log}
 \pause\bigskip
 
-\textbf{Lemma}\\ @{thm t_del_min_log}
+\textbf{Corollary}\\ @{thm t_del_min_log}
 \end{frame}
+\fi
 %-------------------------------------------------------------
 \begin{frame}
 \begin{center}
--- a/Slides/RBT_Slides.thy	Wed Aug 02 17:48:54 2017 +0200
+++ b/Slides/RBT_Slides.thy	Thu Aug 03 09:43:22 2017 +0200
@@ -209,12 +209,13 @@
 \end{frame}
 %-------------------------------------------------------------
 \begin{frame}{Proof in CLRS}
-\includegraphics[scale=0.2,angle=90]{clrsrbti3} \hspace{-1em}
-\includegraphics[scale=0.2,angle=90]{clrsrbti4}
-\vspace{-1em}
+\vspace{-2em}
+\hspace{2em} \includegraphics[scale=0.2]{clrsrbti1}
+\includegraphics[scale=0.19]{clrsrbti2}
+\vspace{-4em}
 
-\includegraphics[scale=0.2,angle=90]{clrsrbti1} \hspace{-1em}
-\includegraphics[scale=0.2,angle=90]{clrsrbti2}
+\hspace{2em} \includegraphics[scale=0.2]{clrsrbti3}
+\includegraphics[scale=0.19]{clrsrbti4}
 \end{frame}
 %-------------------------------------------------------------
 \begin{frame}{Deletion}
--- a/Slides/Sorting_Slides.thy	Wed Aug 02 17:48:54 2017 +0200
+++ b/Slides/Sorting_Slides.thy	Thu Aug 03 09:43:22 2017 +0200
@@ -62,7 +62,7 @@
 \end{tabular}
 \bigskip\pause
 
-Import \texttt{"~~/src/HOL/Library/Multiset"}
+Import \texttt{"\char`\~\char`\~/src/HOL/Library/Multiset"}
 \end{frame}
 %-------------------------------------------------------------
 \section{Insertion Sort}
--- a/Slides/document/prelude.tex	Wed Aug 02 17:48:54 2017 +0200
+++ b/Slides/document/prelude.tex	Thu Aug 03 09:43:22 2017 +0200
@@ -64,7 +64,7 @@
 {\thyfile{#1\char`\_Demo}{#2}}
 
 \newcommand{\afpentry}[1]
-{\filepage{Archive of Formal Proofs}
+{\filepage{\href{https://www.isa-afp.org}{Archive of Formal Proofs}}
 {\url{https://www.isa-afp.org/entries/#1.shtml}}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%