Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Hyperreal/HRealAbs.thy
author paulson
Thu, 04 Jan 2001 10:23:01 +0100
changeset 10778 2c6605049646
parent 10750 a681d3df1a39
child 10919 144ede948e58
permissions -rw-r--r--
more tidying, especially to remove real_of_posnat

(*  Title       : HRealAbs.thy
    Author      : Jacques D. Fleuriot
    Copyright   : 1998  University of Cambridge
    Description : Absolute value function for the hyperreals
*) 

HRealAbs = HyperArith + RealAbs + 

defs
    hrabs_def "abs r  == if (0::hypreal) <=r then r else -r" 

constdefs
  
  hypreal_of_nat :: nat => hypreal                   
  "hypreal_of_nat n     == hypreal_of_real (real_of_nat n)"

end
isabelle