Nominal/FROOT.ML
author Cezary Kaliszyk <cezarykaliszyk@gmail.com>
Tue, 22 May 2012 14:00:59 +0200
changeset 3172 4cf3a4d36799
parent 3116 6968fd7507de
permissions -rw-r--r--
Added workaround for broken quotient_type in tip isabelle.
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