isabelle: src/HOL/Integ/Int.thy@0dbfb578bf75 (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)
8949 d46adac29b71 installing plus_ac0 for int paulson parents: 5582 diff changeset	12	instance int :: plus_ac0 (zadd_commute,zadd_assoc,zadd_zero)
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	wenzelm
	Fri, 28 Sep 2001 19:17:01 +0200
changeset 11626	0dbfb578bf75
parent 11451	8abfb4f7bd02
child 11868	56db9f3a6b3e
permissions	-rw-r--r--