--- 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:
--- 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)