# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1536753103 -3600
# Node ID c73ca43087c0a109722ed4fc6d1d3801b2ce4ec1
# Parent  105bbce656a50383776c4d46705e23817a215b2b
tiny cleanup

diff -r 105bbce656a5 -r c73ca43087c0 src/HOL/Library/Omega_Words_Fun.thy
--- a/src/HOL/Library/Omega_Words_Fun.thy	Tue Sep 11 16:22:04 2018 +0100
+++ b/src/HOL/Library/Omega_Words_Fun.thy	Wed Sep 12 12:51:43 2018 +0100
@@ -219,7 +219,7 @@
 lemma prefix_conc_snd[simp]:
   assumes "n \<ge> length u"
   shows "prefix n (u \<frown> v) = u @ prefix (n - length u) v"
-proof (intro nth_equalityI allI impI)
+proof (intro nth_equalityI)
   show "length (prefix n (u \<frown> v)) = length (u @ prefix (n - length u) v)"
     using assms by simp
   fix i
@@ -258,7 +258,7 @@
   assume ?lhs
   then have 1: "(v\<^sub>1 \<frown> u\<^sub>1) i = (v\<^sub>2 \<frown> u\<^sub>2) i" for i by auto
   show ?rhs
-  proof (intro conjI ext nth_equalityI allI impI)
+  proof (intro conjI ext nth_equalityI)
     show "length v\<^sub>1 = length v\<^sub>2" by (rule assms(1))
   next
     fix i