Nominal/FROOT.ML
author Christian Urban <urbanc@in.tum.de>
Tue, 10 Apr 2012 16:02:30 +0100
changeset 3158 89f9d7e85e88
parent 3116 6968fd7507de
permissions -rw-r--r--
moved lift_raw_const from Quotient to Nominal
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