gcd = Arith +

consts

	divides :: "[nat, nat] => bool"		(infixl 50)
(* Die folgenden Definition bringen Isabelle das Zaehlen bei: *)

consts
	"3"     :: nat               ("3")
	"4"     :: nat               ("4")
	"5"     :: nat               ("5")
	"6"     :: nat               ("6")
	"7"     :: nat               ("7")
	"8"     :: nat               ("8")
        "9"     :: nat               ("9")

translations
	"3" == "Suc(2)"
	"4" == "Suc(3)"
	"5" == "Suc(4)"
	"6" == "Suc(5)"
	"7" == "Suc(6)"
	"8" == "Suc(7)"
        "9" == "Suc(8)"

end