isabelle: src/HOL/Hyperreal/HRealAbs.thy@502a7c95de73 (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
14269 502a7c95de73 conversion of some Real theories to Isar scripts paulson parents: 10919 diff changeset	7	HRealAbs = HyperArith + RealArith +
10750 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	paulson
	Fri, 28 Nov 2003 12:09:37 +0100
changeset 14269	502a7c95de73
parent 10919	144ede948e58
child 14299	0b5c0b0a3eba
permissions	-rw-r--r--