--- a/src/HOL/Nat_Transfer.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Nat_Transfer.thy Wed Aug 10 09:33:54 2016 +0200
@@ -1,4 +1,3 @@
-
(* Authors: Jeremy Avigad and Amine Chaieb *)
section \<open>Generic transfer machinery; specific transfer from nats to ints and back.\<close>
@@ -82,7 +81,7 @@
text \<open>first-order quantifiers\<close>
lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
- by (simp split add: split_nat)
+ by (simp split: split_nat)
lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
proof