src/HOL/NanoJava/ROOT.ML
author berghofe
Mon, 08 Mar 2010 15:00:34 +0100
changeset 35646 b32d6c1bdb4d
parent 33615 261abc2e3155
permissions -rw-r--r--
Added inducts field to inductive_result.

use_thys ["Example"];