src/HOL/TLA/Inc/ROOT.ML
author blanchet
Wed, 02 Jun 2010 12:28:42 +0200
changeset 37318 32b3d16b04f6
parent 33615 261abc2e3155
permissions -rw-r--r--
give more helpful error message

use_thys ["Inc"];