src/HOL/TLA/Memory/ROOT.ML
author huffman
Wed, 03 Mar 2010 21:42:42 -0800
changeset 35572 44eeda8cb708
parent 33615 261abc2e3155
permissions -rw-r--r--
generate lemma take_below, declare chain_take [simp]

use_thys ["MemoryImplementation"];