# HG changeset patch
# User nipkow
# Date 1499534393 -7200
# Node ID 985eb3b647ab5ff06ded180f3e92cba9e5fa90a3
# Parent  d2283b15d2caf4ff26bf3f88a883ca70f8be981d
.

diff -r d2283b15d2ca -r 985eb3b647ab Exercises/ex12/ex12.thy
--- a/Exercises/ex12/ex12.thy	Sat Jul 08 19:03:42 2017 +0200
+++ b/Exercises/ex12/ex12.thy	Sat Jul 08 19:19:53 2017 +0200
@@ -24,8 +24,7 @@
 fun deq :: "'a queue \<Rightarrow> 'a queue" where
 "deq (xs,ys) = balance (xs, tl ys)"
 
-text \<open>Note that we assume that the size computation in \<open>balance\<close> only takes constant time.
-In reality the time is linear. How would you avoid that?\<close>
+text \<open>Again, we count only the newly allocated list cells.\<close>
 
 fun t_enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> nat" where
 "t_enq a (xs,ys) = 1 + (if size xs + 1 \<le> size ys then 0 else size xs + 1 + size ys)"