isabelle: src/HOL/Hyperreal/HRealAbs.thy@213dcc39358f (annotated)

10750 a681d3df1a39 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	1	(* Title : HRealAbs.thy
a681d3df1a39 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	2	Author : Jacques D. Fleuriot
a681d3df1a39 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	3	Copyright : 1998 University of Cambridge
a681d3df1a39 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	4	Description : Absolute value function for the hyperreals
a681d3df1a39 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	5	*)
a681d3df1a39 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	6
a681d3df1a39 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	7	HRealAbs = HyperArith + RealAbs +
a681d3df1a39 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	8
a681d3df1a39 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	9	defs
a681d3df1a39 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	10	hrabs_def "abs r == if (0::hypreal) <=r then r else -r"
a681d3df1a39 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	11
10778 2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10750 diff changeset	12	constdefs
2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10750 diff changeset	13
2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10750 diff changeset	14	hypreal_of_nat :: nat => hypreal
10919 144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real paulson parents: 10778 diff changeset	15	"hypreal_of_nat (n::nat) == hypreal_of_real (real n)"
10778 2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10750 diff changeset	16
10750 a681d3df1a39 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	17	end

author	kleing
	Tue, 13 May 2003 08:59:21 +0200
changeset 14024	213dcc39358f
parent 10919	144ede948e58
child 14269	502a7c95de73
permissions	-rw-r--r--