src/HOL/Nominal/Examples/ROOT.ML
author huffman
Tue, 27 Dec 2011 12:37:11 +0100
changeset 45998 d7cc533ae60d
parent 39616 8052101883c3
permissions -rw-r--r--
remove redundant syntax declaration

use_thys ["Nominal_Examples"];

Unsynchronized.setmp quick_and_dirty true use_thys ["VC_Condition"];