isabelle: src/HOL/Integ/NatBin.thy@50be659d4222 (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
9509 0f3ee1f89ca8 introduction of integer exponentiation paulson parents: 7032 diff changeset	11	NatBin = IntPower +
7032 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
	Fri, 06 Oct 2000 17:35:58 +0200
changeset 10168	50be659d4222
parent 9509	0f3ee1f89ca8
child 10574	8f98f0301d67
permissions	-rw-r--r--