src/HOL/Nominal/Examples/ROOT.ML
changeset 48722 a5e3ba7cbb2a
parent 48721 866f6d5baf4c
child 48723 0829e958f0aa
equal deleted inserted replaced
48721:866f6d5baf4c 48722:a5e3ba7cbb2a
     1 use_thys ["Nominal_Examples"];
       
     2 
       
     3 Unsynchronized.setmp quick_and_dirty true use_thys ["VC_Condition"];