src/HOL/Nominal/Examples/ROOT.ML
author haftmann
Mon, 21 Sep 2009 16:01:30 +0200
changeset 32635 37e32f8aa696
parent 28654 2f9857126498
child 33615 261abc2e3155
permissions -rw-r--r--
added session theory for Nominal_Examples
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19495
3d04b87ad8ba New ROOT file for nominal datatype examples.
berghofe
parents:
diff changeset
     1
32635
37e32f8aa696 added session theory for Nominal_Examples
haftmann
parents: 28654
diff changeset
     2
use_thy "Nominal_Examples";
24895
7cbb842aa99e added two new example files
urbanc
parents: 24153
diff changeset
     3
32635
37e32f8aa696 added session theory for Nominal_Examples
haftmann
parents: 28654
diff changeset
     4
setmp_noncritical quick_and_dirty true use_thy "VC_Condition"; (*FIXME*)