Nominal/FROOT.ML
author webertj
Wed, 27 Mar 2013 16:08:30 +0100
changeset 3214 13ab4f0a0b0e
parent 3116 6968fd7507de
permissions -rw-r--r--
Various changes to support Nominal2 commands in local contexts.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3116
6968fd7507de added FROOT
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
6968fd7507de added FROOT
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
6968fd7507de added FROOT
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
no_document use_thys
6968fd7507de added FROOT
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
   ["Nominal2",
6968fd7507de added FROOT
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
    "Atoms",
6968fd7507de added FROOT
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
    "Eqvt"
6968fd7507de added FROOT
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
   ];
6968fd7507de added FROOT
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
6968fd7507de added FROOT
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
6968fd7507de added FROOT
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10