isabelle: src/HOL/Integ/Int.thy@56db9f3a6b3e (annotated)

5562 02261e6880d1 Renaming of Integ/Integ.* to Integ/Int., and renaming of related constants paulson* parents: diff changeset	1	(* Title: Integ/Int.thy
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int., and renaming of related constants paulson* parents: diff changeset	2	ID: $Id$
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int., and renaming of related constants paulson* parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int., and renaming of related constants paulson* parents: diff changeset	4	Copyright 1998 University of Cambridge
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int., and renaming of related constants paulson* parents: diff changeset	5
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int., and renaming of related constants paulson* parents: diff changeset	6	Type "int" is a linear order
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int., and renaming of related constants paulson* parents: diff changeset	7	*)
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int., and renaming of related constants paulson* parents: diff changeset	8
11451 8abfb4f7bd02 partial restructuring to reduce dependence on Axiom of Choice paulson parents: 9214 diff changeset	9	Int = IntDef +
5562 02261e6880d1 Renaming of Integ/Integ.* to Integ/Int., and renaming of related constants paulson* parents: diff changeset	10
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int., and renaming of related constants paulson* parents: diff changeset	11	instance int :: order (zle_refl,zle_trans,zle_anti_sym,int_less_le)
11868 56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite paulson parents: 11451 diff changeset	12	instance int :: plus_ac0 (zadd_commute,zadd_assoc,zadd_0)
5562 02261e6880d1 Renaming of Integ/Integ.* to Integ/Int., and renaming of related constants paulson* parents: diff changeset	13	instance int :: linorder (zle_linear)
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int., and renaming of related constants paulson* parents: diff changeset	14
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int., and renaming of related constants paulson* parents: diff changeset	15	constdefs
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int., and renaming of related constants paulson* parents: diff changeset	16	nat :: int => nat
11451 8abfb4f7bd02 partial restructuring to reduce dependence on Axiom of Choice paulson parents: 9214 diff changeset	17	"nat(Z) == if neg Z then 0 else (THE m. Z = int m)"
5562 02261e6880d1 Renaming of Integ/Integ.* to Integ/Int., and renaming of related constants paulson* parents: diff changeset	18
9214 9454f30eacc7 Defined abs on int. nipkow parents: 8949 diff changeset	19	defs
9454f30eacc7 Defined abs on int. nipkow parents: 8949 diff changeset	20	zabs_def "abs(i::int) == if i < 0 then -i else i"
9454f30eacc7 Defined abs on int. nipkow parents: 8949 diff changeset	21
5562 02261e6880d1 Renaming of Integ/Integ.* to Integ/Int., and renaming of related constants paulson* parents: diff changeset	22	end

author	paulson
	Mon, 22 Oct 2001 11:54:22 +0200
changeset 11868	56db9f3a6b3e
parent 11451	8abfb4f7bd02
child 13575	ecb6ecd9af13
permissions	-rw-r--r--