isabelle: src/HOL/Real/RealAbs.thy@7eef34adb852 (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
10715 c838477b5c18 more tidying, especially to rationalize the simprules paulson parents: 9429 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
	Sun, 04 Feb 2001 19:31:13 +0100
changeset 11049	7eef34adb852
parent 10715	c838477b5c18
child 11701	3d51fbf81c17
permissions	-rw-r--r--