Nominal/ROOT.ML
author Christian Urban <urbanc@in.tum.de>
Mon, 07 Jun 2010 15:13:39 +0200
changeset 2214 02e03d4287ec
parent 2142 c39d4fe31100
child 2288 3b83960f9544
permissions -rw-r--r--
a bit more in the introduction and abstract
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",
2142
c39d4fe31100 moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat
Christian Urban <urbanc@in.tum.de>
parents: 2137
diff changeset
    16
    "Ex/CoreHaskell",
2122
24ca435ead14 added term4 back to the examples
Christian Urban <urbanc@in.tum.de>
parents: 2120
diff changeset
    17
    "Ex/Test",
24ca435ead14 added term4 back to the examples
Christian Urban <urbanc@in.tum.de>
parents: 2120
diff changeset
    18
    "Manual/Term4"
1604
5ab97f43ec24 More modification needed for compilation
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1485
diff changeset
    19
    ];