isabelle: src/HOL/Integ/NatBin.thy@a901bafe4578 (annotated)

7032 d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	1	(* Title: HOL/NatBin.thy
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	2	ID: $Id$
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	4	Copyright 1999 University of Cambridge
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	5
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	6	Binary arithmetic for the natural numbers
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	7
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	8	This case is simply reduced to that for the non-negative integers
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	9	*)
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	10
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	11	NatBin = IntDiv +
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	12
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	13	instance
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	14	nat :: number
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	15
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	16	defs
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	17	nat_number_of_def
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	18	"number_of v == nat (number_of v)"
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	19	(::bin=>nat ::bin=>int)
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	20
d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	21	end

author	wenzelm
	Mon, 29 Nov 1999 15:52:49 +0100
changeset 8039	a901bafe4578
parent 7032	d6efb3b8e669
child 9509	0f3ee1f89ca8
permissions	-rw-r--r--