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
Fri, 05 Jan 2001 10:17:48 +0100
changeset 10784 27e4d90b35b5
parent 10778 2c6605049646
child 10919 144ede948e58
permissions -rw-r--r--
more removal of obsolete rules

(*  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