README
author Christian Urban <urbanc@in.tum.de>
Thu, 30 Dec 2010 10:00:09 +0000
changeset 2631 e73bd379e839
parent 2568 8193bbaa07fe
child 3070 4b4742aa43f2
child 3204 b69c8660de14
permissions -rw-r--r--
removed local fix for bug in induction_schema; added setup method for strong inductions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
This repository contain a new implementation of
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
Nominal Isabelle.
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
2452
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
     4
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
Subdirectories:
2452
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
     6
===============
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
     7
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
     8
Nominal       ... main files for new Nominal Isabelle
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
     9
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    10
Nominal/Ex    ... examples for new implementation
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    11
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    12
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    13
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    14
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    15
Outher Subdirectories:
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    16
======================
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
1774
c34347ec7ab3 separated general nominal theory into separate folder
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
    18
Attic         ... old version of the quotient package (is now 
c34347ec7ab3 separated general nominal theory into separate folder
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
    19
                  part of the Isabelle distribution)
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    20
1774
c34347ec7ab3 separated general nominal theory into separate folder
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
    21
Literature    ... some relevant papers about binders and
c34347ec7ab3 separated general nominal theory into separate folder
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
    22
                  Core-Haskell
c34347ec7ab3 separated general nominal theory into separate folder
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
    23
2523
e903c32ec24f more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents: 2453
diff changeset
    24
Paper         ... submitted to ESOP
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
2382
e8b9c0ebf5dd added paper by james; some minor cleaning
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
    26
Pearl         ... accepted at ITP 
e8b9c0ebf5dd added paper by james; some minor cleaning
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
    27
Pearl-jv      ... journal version
e8b9c0ebf5dd added paper by james; some minor cleaning
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
    28
2568
8193bbaa07fe merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
Christian Urban <urbanc@in.tum.de>
parents: 2523
diff changeset
    29
Quotient-Paper .. accepted to SAC
2453
Christian Urban <urbanc@in.tum.de>
parents: 2452
diff changeset
    30
Christian Urban <urbanc@in.tum.de>
parents: 2452
diff changeset
    31
Slides        ... various talks Christian gave recently