equal
deleted
inserted
replaced
42 (*>*) |
42 (*>*) |
43 |
43 |
44 section {* Introduction *} |
44 section {* Introduction *} |
45 |
45 |
46 text {* |
46 text {* |
|
47 TODO: write about supp of finite sets |
|
48 |
47 Nominal Isabelle provides a proving infratructure for |
49 Nominal Isabelle provides a proving infratructure for |
48 convenient reasoning about programming languages. At its core Nominal |
50 convenient reasoning about programming languages. At its core Nominal |
49 Isabelle is based on the nominal logic work by Pitts at al |
51 Isabelle is based on the nominal logic work by Pitts at al |
50 \cite{GabbayPitts02,Pitts03}. The most basic notion in this work |
52 \cite{GabbayPitts02,Pitts03}. The most basic notion in this work |
51 is a sort-respecting permutation operation defined over a countably infinite |
53 is a sort-respecting permutation operation defined over a countably infinite |