src/HOL/Imperative_HOL/ex/Linked_Lists.thy

--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri May 13 20:24:10 2016 +0200
@@ -261,7 +261,6 @@
 subsection {* Interaction of these predicates with our heap transitions *}
 
 lemma list_of_set_ref: "refs_of h q rs \<Longrightarrow> p \<notin> set rs \<Longrightarrow> list_of (Ref.set p v h) q as = list_of h q as"
-using assms
 proof (induct as arbitrary: q rs)
   case Nil thus ?case by simp
 next