Pearl/ROOT.ML
author Christian Urban <urbanc@in.tum.de>
Wed, 19 Jan 2011 23:58:12 +0100
changeset 2686 52e1e98edb34
parent 2568 8193bbaa07fe
child 2736 61d30863e5d1
permissions -rw-r--r--
added a very rough version of the tutorial; all seems to work
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2568
8193bbaa07fe merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
Christian Urban <urbanc@in.tum.de>
parents: 2471
diff changeset
     1
no_document use_thys ["../Nominal/Nominal2_Base", 
8193bbaa07fe merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
Christian Urban <urbanc@in.tum.de>
parents: 2471
diff changeset
     2
                      "../Nominal/Nominal2_Eqvt",
8193bbaa07fe merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
Christian Urban <urbanc@in.tum.de>
parents: 2471
diff changeset
     3
                      "../Nominal/Atoms", 
1772
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
                      "LaTeXsugar"];
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
use_thys ["Paper"];