Nominal/ROOT.ML
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Mon, 10 May 2010 15:45:04 +0200
changeset 2093 751d1349329b
parent 2083 9568f9f31822
child 2120 2786ff1df475
permissions -rw-r--r--
merge
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1261
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
quick_and_dirty := true;
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
no_document use_thys
1797
fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents: 1795
diff changeset
     4
   ["Ex/Lambda",
2083
9568f9f31822 tuned file names for examples
Christian Urban <urbanc@in.tum.de>
parents: 2062
diff changeset
     5
    "Ex/LF",
1911
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy
Christian Urban <urbanc@in.tum.de>
parents: 1797
diff changeset
     6
    "Ex/SingleLet",
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1656
diff changeset
     7
    "Ex/Ex1rec",
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1656
diff changeset
     8
    "Ex/Ex2",
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1656
diff changeset
     9
    "Ex/Ex3",
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1656
diff changeset
    10
    "Ex/ExLet",
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1656
diff changeset
    11
    "Ex/ExLetRec",
1795
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
    12
    "Ex/TypeSchemes",
2083
9568f9f31822 tuned file names for examples
Christian Urban <urbanc@in.tum.de>
parents: 2062
diff changeset
    13
    "Ex/Modules",
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1656
diff changeset
    14
    "Ex/ExPS3",
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1656
diff changeset
    15
    "Ex/ExPS7",
2083
9568f9f31822 tuned file names for examples
Christian Urban <urbanc@in.tum.de>
parents: 2062
diff changeset
    16
    "Ex/CoreHaskell",
2062
65bdcc42badd "isabelle make" compiles all examples with newparser/newfv/newalpha only.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1911
diff changeset
    17
    "Ex/Test",
65bdcc42badd "isabelle make" compiles all examples with newparser/newfv/newalpha only.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1911
diff changeset
    18
    "Manual/Term4"
1604
5ab97f43ec24 More modification needed for compilation
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1485
diff changeset
    19
    ];