--- a/src/ZF/Int_ZF.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/ZF/Int_ZF.thy Wed Aug 10 09:33:54 2016 +0200
@@ -283,7 +283,7 @@
by (simp add: nat_of_def)
lemma nat_of_congruent: "(\<lambda>x. (\<lambda>\<langle>x,y\<rangle>. x #- y)(x)) respects intrel"
-by (auto simp add: congruent_def split add: nat_diff_split)
+by (auto simp add: congruent_def split: nat_diff_split)
lemma raw_nat_of:
"[| x\<in>nat; y\<in>nat |] ==> raw_nat_of(intrel``{<x,y>}) = x#-y"
@@ -367,7 +367,7 @@
apply (subgoal_tac "intify(z) \<in> int")
apply (simp add: int_def)
apply (auto simp add: znegative nat_of_def raw_nat_of
- split add: nat_diff_split)
+ split: nat_diff_split)
done