src/HOL/NanoJava/ROOT.ML
author wenzelm
Wed, 14 May 2008 11:16:11 +0200
changeset 26886 d43264d547f8
parent 11565 ab004c0ecc63
child 33615 261abc2e3155
permissions -rw-r--r--
use_text: added str_of_pos argument (ignored);

use_thy "Example";