nominal2: README@66114fa3d2ee (annotated)

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
3235 5ebd327ffb96 changed nominal_primrec into the more appropriate nominal_function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3212 diff changeset	9	The version of Nominal2 in the AFP can be tested with
5ebd327ffb96 changed nominal_primrec into the more appropriate nominal_function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3212 diff changeset	10
5ebd327ffb96 changed nominal_primrec into the more appropriate nominal_function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3212 diff changeset	11	isabelle build -d . Nominal2
5ebd327ffb96 changed nominal_primrec into the more appropriate nominal_function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3212 diff changeset	12	isabelle build -d . Launchbury
5ebd327ffb96 changed nominal_primrec into the more appropriate nominal_function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3212 diff changeset	13
5ebd327ffb96 changed nominal_primrec into the more appropriate nominal_function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3212 diff changeset	14
2452 39f8d405d7a2 updated todos Christian Urban <urbanc@in.tum.de> parents: 2382 diff changeset	15
1773 c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	Subdirectories:
2452 39f8d405d7a2 updated todos Christian Urban <urbanc@in.tum.de> parents: 2382 diff changeset	17	===============
39f8d405d7a2 updated todos Christian Urban <urbanc@in.tum.de> parents: 2382 diff changeset	18
39f8d405d7a2 updated todos Christian Urban <urbanc@in.tum.de> parents: 2382 diff changeset	19	Nominal ... main files for new Nominal Isabelle
39f8d405d7a2 updated todos Christian Urban <urbanc@in.tum.de> parents: 2382 diff changeset	20
39f8d405d7a2 updated todos Christian Urban <urbanc@in.tum.de> parents: 2382 diff changeset	21	Nominal/Ex ... examples for new implementation
39f8d405d7a2 updated todos Christian Urban <urbanc@in.tum.de> parents: 2382 diff changeset	22
39f8d405d7a2 updated todos Christian Urban <urbanc@in.tum.de> parents: 2382 diff changeset	23
3207 d3f7c8cce53b updated README Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3205 diff changeset	24	Other Subdirectories:
d3f7c8cce53b updated README Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3205 diff changeset	25	=====================
1773 c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: diff changeset	26
1774 c34347ec7ab3 separated general nominal theory into separate folder Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	27	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	28	part of the Isabelle distribution)
1773 c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: diff changeset	29
1774 c34347ec7ab3 separated general nominal theory into separate folder Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	30	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	31	Core-Haskell
c34347ec7ab3 separated general nominal theory into separate folder Christian Urban <urbanc@in.tum.de> parents: 1773 diff changeset	32
3205 645ee5189bec tuned Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3204 diff changeset	33	Paper ... accepted at ESOP
1773 c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: diff changeset	34
2382 e8b9c0ebf5dd added paper by james; some minor cleaning Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	35	Pearl ... accepted at ITP
3205 645ee5189bec tuned Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3204 diff changeset	36	Pearl-jv ... accepted at LMCS
2382 e8b9c0ebf5dd added paper by james; some minor cleaning Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	37
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	38	Quotient-Paper .. accepted to SAC
2453 2f47291b6ff9 tuned Christian Urban <urbanc@in.tum.de> parents: 2452 diff changeset	39
3207 d3f7c8cce53b updated README Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3205 diff changeset	40	Slides ... various talks Christian gave recently
d3f7c8cce53b updated README Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3205 diff changeset	41
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	Mercurial
d3f7c8cce53b updated README Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3205 diff changeset	44	=========
d3f7c8cce53b updated README Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3205 diff changeset	45
d3f7c8cce53b updated README Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3205 diff changeset	46	creating a new branch
d3f7c8cce53b updated README Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3205 diff changeset	47	hg branch Nominal2-IsabelleXXXX
d3f7c8cce53b updated README Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3205 diff changeset	48
d3f7c8cce53b updated README Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3205 diff changeset	49	returning to default branch
d3f7c8cce53b updated README Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 3205 diff changeset	50	hg update default

author	Christian Urban <urbanc@in.tum.de>
	Thu, 19 Apr 2018 13:58:22 +0100
branch	Nominal2-Isabelle2016-1
changeset 3246	66114fa3d2ee
parent 3235	5ebd327ffb96
permissions	-rw-r--r--