floor and ceiling definitions are not code equations -- this enables trivial evaluation of floor and ceiling
(* Title: LCF/ex/ROOT.ML
Author: Tobias Nipkow
Copyright 1991 University of Cambridge
Some examples from Lawrence Paulson's book Logic and Computation.
*)
use_thys ["Ex1", "Ex2", "Ex3", "Ex4"];