# HG changeset patch
# User wenzelm
# Date 1460461777 -7200
# Node ID a9c40cf517d11e0741cd637531cc1282d848ca6c
# Parent  bb3986d955621a4ea636b9b0c6df919dbe869571
tuned;

diff -r bb3986d95562 -r a9c40cf517d1 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Mon Apr 11 15:50:50 2016 +0200
+++ b/src/HOL/Transitive_Closure.thy	Tue Apr 12 13:49:37 2016 +0200
@@ -534,7 +534,7 @@
 lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+"
   by (blast elim: tranclE dest: trancl_into_rtrancl)
 
-lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y"
+lemma irrefl_trancl_rD: "\<forall>x. (x, x) \<notin> r^+ \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> x \<noteq> y"
   by (blast dest: r_into_trancl)
 
 lemma trancl_subset_Sigma_aux:
diff -r bb3986d95562 -r a9c40cf517d1 src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Mon Apr 11 15:50:50 2016 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy	Tue Apr 12 13:49:37 2016 +0200
@@ -993,7 +993,7 @@
 lemma bin_rsplit_size_sign' [rule_format] : 
   "\<lbrakk>n > 0; rev sw = bin_rsplit n (nw, w)\<rbrakk> \<Longrightarrow> 
     (ALL v: set sw. bintrunc n v = v)"
-  apply (induct sw arbitrary: nw w v)
+  apply (induct sw arbitrary: nw w)
    apply clarsimp
   apply clarsimp
   apply (drule bthrs)