Nominal/ROOT.ML
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Thu, 29 Apr 2010 16:18:38 +0200
changeset 1988 4444d52201dc
parent 1911 60b5c61d3de2
child 2062 65bdcc42badd
permissions -rw-r--r--
Fixing the definitions in the Parser.
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",
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1656
diff changeset
     5
    "Ex/ExLF",
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",
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1656
diff changeset
    13
    "Ex/ExLeroy",
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",
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1656
diff changeset
    16
    "Ex/ExCoreHaskell",
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1656
diff changeset
    17
    "Ex/Test"
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1656
diff changeset
    18
(*  "Ex/ExPS6", *)
1604
5ab97f43ec24 More modification needed for compilation
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1485
diff changeset
    19
    ];