isabelle: src/HOL/Real/RealAbs.thy@2e1dca5af2d4 (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
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8856 diff changeset	12	abs_real_def "abs r == (if (#0::real) <= r then r else -r)"
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
	Wed, 30 Aug 2000 13:54:53 +0200
changeset 9738	2e1dca5af2d4
parent 9429	8ebc549e9326
child 10715	c838477b5c18
permissions	-rw-r--r--