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