isabelle: src/HOL/Hyperreal/HRealAbs.thy@48dc606749bd (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
10778 2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10750 diff changeset	9	constdefs
2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10750 diff changeset	10
2c6605049646 more tidying, especially to remove real_of_posnat paulson parents: 10750 diff changeset	11	hypreal_of_nat :: nat => hypreal
10919 144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real paulson parents: 10778 diff changeset	12	"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	13
10750 a681d3df1a39 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	14	end

author	paulson
	Thu, 18 Dec 2003 15:06:24 +0100
changeset 14301	48dc606749bd
parent 14299	0b5c0b0a3eba
child 14365	3d4df8c166ae
permissions	-rw-r--r--