src/HOL/base.ML
author nipkow
Mon, 09 Feb 2009 18:50:10 +0100
changeset 29849 a2baf1b221be
parent 29505 c6d2d23909d1
child 30929 d9343c0aac11
permissions -rw-r--r--
new attribute "arith" for facts supplied to arith.

(*side-entry for HOL-Base*)
use_thy "Code_Setup";