| author | Christian Urban <christian dot urban at kcl dot ac dot uk> | 
| Thu, 29 Nov 2012 21:59:38 +0000 | |
| changeset 3204 | b69c8660de14 | 
| parent 2568 | 8193bbaa07fe | 
| child 3205 | 645ee5189bec | 
| permissions | -rw-r--r-- | 
| 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 | |
| 3204 
b69c8660de14
fixed problem with not fresh enough permutation name in nominal_primrec
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
2568diff
changeset | 4 | Compilation of Tests | 
| 
b69c8660de14
fixed problem with not fresh enough permutation name in nominal_primrec
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
2568diff
changeset | 5 | ==================== | 
| 
b69c8660de14
fixed problem with not fresh enough permutation name in nominal_primrec
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
2568diff
changeset | 6 | |
| 
b69c8660de14
fixed problem with not fresh enough permutation name in nominal_primrec
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
2568diff
changeset | 7 | isabelle build -d . -g Tests | 
| 
b69c8660de14
fixed problem with not fresh enough permutation name in nominal_primrec
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
2568diff
changeset | 8 | |
| 2452 | 9 | |
| 1773 
c0eac04ae3b4
added README and moved examples into separate directory
 Christian Urban <urbanc@in.tum.de> parents: diff
changeset | 10 | Subdirectories: | 
| 2452 | 11 | =============== | 
| 12 | ||
| 13 | Nominal ... main files for new Nominal Isabelle | |
| 14 | ||
| 15 | Nominal/Ex ... examples for new implementation | |
| 16 | ||
| 17 | ||
| 18 | ||
| 19 | ||
| 20 | Outher Subdirectories: | |
| 21 | ====================== | |
| 1773 
c0eac04ae3b4
added README and moved examples into separate directory
 Christian Urban <urbanc@in.tum.de> parents: diff
changeset | 22 | |
| 1774 
c34347ec7ab3
separated general nominal theory into separate folder
 Christian Urban <urbanc@in.tum.de> parents: 
1773diff
changeset | 23 | Attic ... old version of the quotient package (is now | 
| 
c34347ec7ab3
separated general nominal theory into separate folder
 Christian Urban <urbanc@in.tum.de> parents: 
1773diff
changeset | 24 | part of the Isabelle distribution) | 
| 1773 
c0eac04ae3b4
added README and moved examples into separate directory
 Christian Urban <urbanc@in.tum.de> parents: diff
changeset | 25 | |
| 1774 
c34347ec7ab3
separated general nominal theory into separate folder
 Christian Urban <urbanc@in.tum.de> parents: 
1773diff
changeset | 26 | Literature ... some relevant papers about binders and | 
| 
c34347ec7ab3
separated general nominal theory into separate folder
 Christian Urban <urbanc@in.tum.de> parents: 
1773diff
changeset | 27 | Core-Haskell | 
| 
c34347ec7ab3
separated general nominal theory into separate folder
 Christian Urban <urbanc@in.tum.de> parents: 
1773diff
changeset | 28 | |
| 2523 
e903c32ec24f
more on the pearl paper
 Christian Urban <urbanc@in.tum.de> parents: 
2453diff
changeset | 29 | Paper ... submitted to ESOP | 
| 1773 
c0eac04ae3b4
added README and moved examples into separate directory
 Christian Urban <urbanc@in.tum.de> parents: diff
changeset | 30 | |
| 2382 
e8b9c0ebf5dd
added paper by james; some minor cleaning
 Christian Urban <urbanc@in.tum.de> parents: 
1774diff
changeset | 31 | Pearl ... accepted at ITP | 
| 
e8b9c0ebf5dd
added paper by james; some minor cleaning
 Christian Urban <urbanc@in.tum.de> parents: 
1774diff
changeset | 32 | Pearl-jv ... journal version | 
| 
e8b9c0ebf5dd
added paper by james; some minor cleaning
 Christian Urban <urbanc@in.tum.de> parents: 
1774diff
changeset | 33 | |
| 2568 
8193bbaa07fe
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
 Christian Urban <urbanc@in.tum.de> parents: 
2523diff
changeset | 34 | Quotient-Paper .. accepted to SAC | 
| 2453 | 35 | |
| 36 | Slides ... various talks Christian gave recently |