isabelle: src/HOL/Real/RealAbs.thy@ce180e5b7fa0 (annotated)

5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	1	(* Title : RealAbs.thy
7219 4e3f386c2e37 inserted Id: lines paulson parents: 5588 diff changeset	2	ID : $Id$
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	3	Author : Jacques D. Fleuriot
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	4	Copyright : 1998 University of Cambridge
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	5	Description : Absolute value function for the reals
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	6	*)
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	7
9429 8ebc549e9326 changed deps; wenzelm parents: 9013 diff changeset	8	RealAbs = RealArith +
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	9
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8856 diff changeset	10
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8856 diff changeset	11	defs
12018 ec054019c910 Numerals and simprocs for types real and hypreal. The abstract paulson parents: 11701 diff changeset	12	real_abs_def "abs r == (if (0::real) <= r then r else -r)"
9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8856 diff changeset	13
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7334 diff changeset	14	end

author	wenzelm
	Fri, 08 Mar 2002 16:24:06 +0100
changeset 13049	ce180e5b7fa0
parent 12018	ec054019c910
child 14265	95b42e69436c
permissions	-rw-r--r--