equal
deleted
inserted
replaced
1 |
1 |
2 header {* |
2 (* |
3 |
3 |
4 Nominal Isabelle Tutorial at POPL'11 |
4 Nominal Isabelle Tutorial at POPL'11 |
5 ==================================== |
5 ==================================== |
6 |
6 |
7 Nominal Isabelle is a definitional extension of Isabelle/HOL, which |
7 Nominal Isabelle is a definitional extension of Isabelle/HOL, which |
57 |
57 |
58 For nominal the following two symbols have a special meaning |
58 For nominal the following two symbols have a special meaning |
59 |
59 |
60 \<sharp> sharp (freshness) |
60 \<sharp> sharp (freshness) |
61 \<bullet> bullet (permutation application) |
61 \<bullet> bullet (permutation application) |
62 *} |
62 *) |
63 |
63 |
64 theory Tutorial1s |
64 theory Tutorial1s |
65 imports Lambda |
65 imports Lambda |
66 begin |
66 begin |
67 |
67 |