isabelle: src/HOL/Real/RealAbs.thy@983d2db52062 (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
11701 3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, wenzelm parents: 10715 diff changeset	12	real_abs_def "abs r == (if (Numeral0::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
	Mon, 15 Oct 2001 20:31:18 +0200
changeset 11773	983d2db52062
parent 11701	3d51fbf81c17
child 12018	ec054019c910
permissions	-rw-r--r--