--- a/src/ZF/Arith.thy Sun Jul 14 15:11:21 2002 +0200
+++ b/src/ZF/Arith.thy Sun Jul 14 15:14:43 2002 +0200
@@ -87,7 +87,7 @@
lemmas zero_lt_natE = zero_lt_lemma [THEN bexE, standard]
-(** natify: coercion to "nat" **)
+subsection{*@{text natify}, the Coercion to @{term nat}*}
lemma pred_succ_eq [simp]: "pred(succ(y)) = y"
by (unfold pred_def, auto)
@@ -163,7 +163,7 @@
by (simp add: div_def)
-(*** Typing rules ***)
+subsection{*Typing rules*}
(** Addition **)
@@ -218,7 +218,7 @@
done
-(*** Addition ***)
+subsection{*Addition*}
(*Natify has weakened this law, compared with the older approach*)
lemma add_0_natify [simp]: "0 #+ m = natify(m)"
@@ -308,7 +308,7 @@
by (drule add_lt_elim1_natify, auto)
-(*** Monotonicity of Addition ***)
+subsection{*Monotonicity of Addition*}
(*strict, in 1st argument; proof is by rule induction on 'less than'.
Still need j:nat, for consider j = omega. Then we can have i<omega,
@@ -402,7 +402,7 @@
by auto
-(*** Multiplication [the simprocs need these laws] ***)
+subsection{*Multiplication*}
lemma mult_0 [simp]: "0 #* m = 0"
by (simp add: mult_def)