Nominal/ROOT.ML
author Christian Urban <urbanc@in.tum.de>
Fri, 16 Jul 2010 05:09:45 +0100
changeset 2364 2bf351f09317
parent 2330 8728f7990f6d
child 2440 0a36825b16c1
permissions -rw-r--r--
submitted version
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
2330
8728f7990f6d merged cezary's changes
Christian Urban <urbanc@in.tum.de>
parents: 2288
diff changeset
     3
(*
1261
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
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
     5
   ["Ex/Lambda",
2083
9568f9f31822 tuned file names for examples
Christian Urban <urbanc@in.tum.de>
parents: 2062
diff changeset
     6
    "Ex/LF",
1911
60b5c61d3de2 renamed Ex1.thy to SingleLet.thy
Christian Urban <urbanc@in.tum.de>
parents: 1797
diff changeset
     7
    "Ex/SingleLet",
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1656
diff changeset
     8
    "Ex/Ex1rec",
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1656
diff changeset
     9
    "Ex/Ex2",
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1656
diff changeset
    10
    "Ex/Ex3",
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1656
diff changeset
    11
    "Ex/ExLet",
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1656
diff changeset
    12
    "Ex/ExLetRec",
1795
e39453c8b186 tuned type-schemes example
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
    13
    "Ex/TypeSchemes",
2083
9568f9f31822 tuned file names for examples
Christian Urban <urbanc@in.tum.de>
parents: 2062
diff changeset
    14
    "Ex/Modules",
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1656
diff changeset
    15
    "Ex/ExPS3",
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents: 1656
diff changeset
    16
    "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
    17
    "Ex/CoreHaskell",
2288
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents: 2142
diff changeset
    18
    "Ex/Test"(*,
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents: 2142
diff changeset
    19
    "Manual/Term4"*)
1604
5ab97f43ec24 More modification needed for compilation
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1485
diff changeset
    20
    ];
2330
8728f7990f6d merged cezary's changes
Christian Urban <urbanc@in.tum.de>
parents: 2288
diff changeset
    21
*)