isabelle: src/HOL/Nominal/Examples/Lambda_mu.thy@ce724d5bada2 (annotated)

18269 3f36e2165e51 some small tuning urbanc parents: 18106 diff changeset	1	(* $Id$ *)
18106 836135c8acb2 Initial commit. urbanc parents: diff changeset	2
836135c8acb2 Initial commit. urbanc parents: diff changeset	3	theory lambda_mu
836135c8acb2 Initial commit. urbanc parents: diff changeset	4	imports "../nominal"
836135c8acb2 Initial commit. urbanc parents: diff changeset	5	begin
836135c8acb2 Initial commit. urbanc parents: diff changeset	6
18269 3f36e2165e51 some small tuning urbanc parents: 18106 diff changeset	7	section {* Lambda-Mu according to a paper by Gavin Bierman *}
18106 836135c8acb2 Initial commit. urbanc parents: diff changeset	8
836135c8acb2 Initial commit. urbanc parents: diff changeset	9	atom_decl var mvar
836135c8acb2 Initial commit. urbanc parents: diff changeset	10
836135c8acb2 Initial commit. urbanc parents: diff changeset	11	nominal_datatype trm = Var "var"
836135c8acb2 Initial commit. urbanc parents: diff changeset	12	\| Lam "\<guillemotleft>var\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
836135c8acb2 Initial commit. urbanc parents: diff changeset	13	\| App "trm" "trm"
836135c8acb2 Initial commit. urbanc parents: diff changeset	14	\| Pss "mvar" "trm"
836135c8acb2 Initial commit. urbanc parents: diff changeset	15	\| Act "\<guillemotleft>mvar\<guillemotright>trm" ("Act [_]._" [100,100] 100)
836135c8acb2 Initial commit. urbanc parents: diff changeset	16