author | wenzelm |
Sun, 16 Jan 2011 15:53:03 +0100 | |
changeset 41589 | bbd861837ebc |
parent 25867 | c24395ea4e71 |
child 63167 | 0909deb8059b |
permissions | -rw-r--r-- |
19501 | 1 |
theory Lambda_mu |
25867 | 2 |
imports "../Nominal" |
18106 | 3 |
begin |
4 |
||
18269 | 5 |
section {* Lambda-Mu according to a paper by Gavin Bierman *} |
18106 | 6 |
|
7 |
atom_decl var mvar |
|
8 |
||
22829
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
19501
diff
changeset
|
9 |
nominal_datatype trm = |
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
19501
diff
changeset
|
10 |
Var "var" |
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
19501
diff
changeset
|
11 |
| Lam "\<guillemotleft>var\<guillemotright>trm" ("Lam [_]._" [100,100] 100) |
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
19501
diff
changeset
|
12 |
| App "trm" "trm" |
25867 | 13 |
| Pss "mvar" "trm" (* passivate *) |
14 |
| Act "\<guillemotleft>mvar\<guillemotright>trm" ("Act [_]._" [100,100] 100) (* activate *) |
|
15 |
||
18106 | 16 |
|
19501 | 17 |
end |