src/ZF/Arith.thy
changeset 13328 703de709a64b
parent 13185 da61bfa0a391
child 13356 c9cfe1638bf2
--- a/src/ZF/Arith.thy	Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Arith.thy	Tue Jul 09 23:05:26 2002 +0200
@@ -3,9 +3,6 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-Arithmetic operators and their definitions
-
-Proofs about elementary arithmetic: addition, multiplication, etc.
 *)
 
 (*"Difference" is subtraction of natural numbers.
@@ -14,8 +11,12 @@
   Also, rec(m, 0, %z w.z) is pred(m).   
 *)
 
+header{*Arithmetic Operators and Their Definitions*} 
+
 theory Arith = Univ:
 
+text{*Proofs about elementary arithmetic: addition, multiplication, etc.*}
+
 constdefs
   pred   :: "i=>i"    (*inverse of succ*)
     "pred(y) == THE x. y = succ(x)"