--- a/src/ZF/Arith.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/Arith.thy Sat Nov 01 14:20:38 2014 +0100
@@ -413,12 +413,12 @@
"i \<in> nat ==> pred(i) \<in> nat"
by (simp add: pred_def split: split_nat_case)
-lemma nat_diff_pred: "[|i\<in>nat; j\<in>nat|] ==> i #- succ(j) = pred(i #- j)";
+lemma nat_diff_pred: "[|i\<in>nat; j\<in>nat|] ==> i #- succ(j) = pred(i #- j)"
apply (rule_tac m=i and n=j in diff_induct)
apply (auto simp add: pred_def nat_imp_quasinat split: split_nat_case)
done
-lemma diff_succ_eq_pred: "i #- succ(j) = pred(i #- j)";
+lemma diff_succ_eq_pred: "i #- succ(j) = pred(i #- j)"
apply (insert nat_diff_pred [of "natify(i)" "natify(j)"])
apply (simp add: natify_succ [symmetric])
done
@@ -435,7 +435,7 @@
text{*We actually prove @{term "i #- j #- k = i #- (j #+ k)"}*}
lemma diff_diff_left [simplified]:
- "natify(i)#-natify(j)#-k = natify(i) #- (natify(j)#+k)";
+ "natify(i)#-natify(j)#-k = natify(i) #- (natify(j)#+k)"
by (rule_tac m="natify(i)" and n="natify(j)" in diff_induct, auto)