isabelle: src/HOL/Integ/Int.thy@50be659d4222 (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
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int., and renaming of related constants paulson* parents: diff changeset	9	Int = IntDef +
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
5582 a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations paulson parents: 5562 diff changeset	17	"nat(Z) == if neg Z then 0 else (@ 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, 06 Oct 2000 17:35:58 +0200
changeset 10168	50be659d4222
parent 9214	9454f30eacc7
child 11451	8abfb4f7bd02
permissions	-rw-r--r--