| author | nipkow |
| Sat, 16 Jun 2007 15:01:54 +0200 | |
| changeset 23400 | a64b39e5809b |
| parent 22829 | f1db55c7534d |
| child 25867 | c24395ea4e71 |
| permissions | -rw-r--r-- |
| 18269 | 1 |
(* $Id$ *) |
| 18106 | 2 |
|
| 19501 | 3 |
theory Lambda_mu |
4 |
imports "../Nominal" |
|
| 18106 | 5 |
begin |
6 |
||
| 18269 | 7 |
section {* Lambda-Mu according to a paper by Gavin Bierman *}
|
| 18106 | 8 |
|
9 |
atom_decl var mvar |
|
10 |
||
|
22829
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
19501
diff
changeset
|
11 |
nominal_datatype trm = |
|
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
19501
diff
changeset
|
12 |
Var "var" |
|
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
19501
diff
changeset
|
13 |
| 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
|
14 |
| App "trm" "trm" |
|
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
19501
diff
changeset
|
15 |
| Pss "mvar" "trm" |
|
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
19501
diff
changeset
|
16 |
| Act "\<guillemotleft>mvar\<guillemotright>trm" ("Act [_]._" [100,100] 100)
|
| 18106 | 17 |
|
| 19501 | 18 |
end |