| author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
| Fri, 06 Sep 2013 10:06:41 +0100 | |
| changeset 3223 | c9a1c6f50ff5 |
| parent 3212 | 0f76f481dbb5 |
| child 3235 | 5ebd327ffb96 |
| 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:
2568
diff
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:
2568
diff
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:
2568
diff
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:
2568
diff
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:
2568
diff
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 |
||
|
3207
d3f7c8cce53b
updated README
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3205
diff
changeset
|
18 |
Other Subdirectories: |
|
d3f7c8cce53b
updated README
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3205
diff
changeset
|
19 |
===================== |
|
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 |
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
|
22 |
part of the Isabelle distribution) |
|
1773
c0eac04ae3b4
added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
23 |
|
|
1774
c34347ec7ab3
separated general nominal theory into separate folder
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
24 |
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
|
25 |
Core-Haskell |
|
c34347ec7ab3
separated general nominal theory into separate folder
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
26 |
|
|
3205
645ee5189bec
tuned
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3204
diff
changeset
|
27 |
Paper ... accepted at ESOP |
|
1773
c0eac04ae3b4
added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
28 |
|
|
2382
e8b9c0ebf5dd
added paper by james; some minor cleaning
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
29 |
Pearl ... accepted at ITP |
|
3205
645ee5189bec
tuned
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3204
diff
changeset
|
30 |
Pearl-jv ... accepted at LMCS |
|
2382
e8b9c0ebf5dd
added paper by james; some minor cleaning
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
31 |
|
|
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
|
32 |
Quotient-Paper .. accepted to SAC |
| 2453 | 33 |
|
|
3207
d3f7c8cce53b
updated README
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3205
diff
changeset
|
34 |
Slides ... various talks Christian gave recently |
|
d3f7c8cce53b
updated README
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3205
diff
changeset
|
35 |
|
|
d3f7c8cce53b
updated README
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3205
diff
changeset
|
36 |
|
|
d3f7c8cce53b
updated README
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3205
diff
changeset
|
37 |
Mercurial |
|
d3f7c8cce53b
updated README
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3205
diff
changeset
|
38 |
========= |
|
d3f7c8cce53b
updated README
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3205
diff
changeset
|
39 |
|
|
d3f7c8cce53b
updated README
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3205
diff
changeset
|
40 |
creating a new branch |
|
d3f7c8cce53b
updated README
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3205
diff
changeset
|
41 |
hg branch Nominal2-IsabelleXXXX |
|
d3f7c8cce53b
updated README
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3205
diff
changeset
|
42 |
|
|
d3f7c8cce53b
updated README
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3205
diff
changeset
|
43 |
returning to default branch |
|
d3f7c8cce53b
updated README
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3205
diff
changeset
|
44 |
hg update default |