isabelle: src/HOL/Integ/IntPower.thy@50be659d4222 (annotated)

9509 0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	1	(* Title: IntPower.thy
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	2	ID: $Id$
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	3	Author: Thomas M. Rasmussen
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	4	Copyright 2000 University of Cambridge
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	5
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	6	Integer powers
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	7	*)
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	8
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	9	IntPower = IntDiv +
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	10
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	11	instance
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	12	int :: {power}
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	13
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	14	primrec
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	15	power_0 "p ^ 0 = #1"
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	16	power_Suc "p ^ (Suc n) = (p::int) * (p ^ n)"
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	17
0f3ee1f89ca8 introduction of integer exponentiation paulson parents: diff changeset	18	end

author	wenzelm
	Fri, 06 Oct 2000 17:35:58 +0200
changeset 10168	50be659d4222
parent 9509	0f3ee1f89ca8
child 11701	3d51fbf81c17
permissions	-rw-r--r--