isabelle: src/HOL/Integ/NatBin.thy@b301d1f72552 (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
10574 8f98f0301d67 Linear arithmetic now copes with mixed nat/int formulae. nipkow parents: 9509 diff changeset	11	theory NatBin = IntPower
8f98f0301d67 Linear arithmetic now copes with mixed nat/int formulae. nipkow parents: 9509 diff changeset	12	files ("nat_bin.ML"):
7032 d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	13
10574 8f98f0301d67 Linear arithmetic now copes with mixed nat/int formulae. nipkow parents: 9509 diff changeset	14	instance nat :: number ..
7032 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
10574 8f98f0301d67 Linear arithmetic now copes with mixed nat/int formulae. nipkow parents: 9509 diff changeset	17	nat_number_of_def:
7032 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
10574 8f98f0301d67 Linear arithmetic now copes with mixed nat/int formulae. nipkow parents: 9509 diff changeset	21	use "nat_bin.ML" setup nat_bin_arith_setup
8f98f0301d67 Linear arithmetic now copes with mixed nat/int formulae. nipkow parents: 9509 diff changeset	22
7032 d6efb3b8e669 NatBin: binary arithmetic for the naturals paulson parents: diff changeset	23	end

author	wenzelm
	Mon, 12 Feb 2001 20:43:12 +0100
changeset 11099	b301d1f72552
parent 10574	8f98f0301d67
child 11464	ddea204de5bc
permissions	-rw-r--r--