src/HOL/NanoJava/ROOT.ML
author bulwahn
Sat, 09 Jul 2011 19:28:33 +0200
changeset 43733 a6ca7b83612f
parent 33615 261abc2e3155
permissions -rw-r--r--
adding code equations to execute floor and ceiling on rational and real numbers

use_thys ["Example"];