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 wenzelm
Sat, 01 Sep 2001 00:14:16 +0200
changeset 11543 d61b913431c5
parent 10919 144ede948e58
child 14269 502a7c95de73
permissions -rw-r--r--
renamed `keep_derivs' to `proofs', and made an integer;

(*  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::nat) == hypreal_of_real (real n)"

end
isabelle