src/HOL/NSA/Hypercomplex.thy
author huffman
Fri, 02 Sep 2011 20:58:31 -0700
changeset 44678 21eb31192850
parent 27468 0783dd1dc13d
permissions -rw-r--r--
remove redundant simp rules ceiling_floor and floor_ceiling

theory Hypercomplex
imports CLim Hyperreal
begin

end