src/HOL/Nominal/Examples/ROOT.ML
author wenzelm
Sat, 03 Dec 2011 13:11:50 +0100
changeset 45744 0ad063afa3d6
parent 39616 8052101883c3
permissions -rw-r--r--
caret_range based on BreakIterator, which handles combined unicode characters as well;

use_thys ["Nominal_Examples"];

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