src/HOL/TLA/Memory/ROOT.ML
author berghofe
Tue, 04 May 2010 14:11:28 +0200
changeset 36643 f36588af1ba1
parent 33615 261abc2e3155
permissions -rw-r--r--
Turned Sem into an inductive definition.

use_thys ["MemoryImplementation"];