src/HOL/base.ML
author blanchet
Mon, 09 Feb 2009 12:31:36 +0100
changeset 29868 787349bb53e9
parent 29505 c6d2d23909d1
child 30929 d9343c0aac11
permissions -rw-r--r--
Reintroduced nitpick_ind_intro attribute. It looks like I need it nonetheless.

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