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

18269 3f36e2165e51 some small tuning urbanc parents: 18106 diff changeset	1	(* $Id$ *)
18106 836135c8acb2 Initial commit. urbanc parents: diff changeset	2
19501 9afa7183dfc2 Capitalized theory names. berghofe parents: 18659 diff changeset	3	theory Lambda_mu
25867 c24395ea4e71 tuned proofs urbanc parents: 22829 diff changeset	4	imports "../Nominal"
18106 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
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"
25867 c24395ea4e71 tuned proofs urbanc parents: 22829 diff changeset	15	\| Pss "mvar" "trm" (* passivate *)
c24395ea4e71 tuned proofs urbanc parents: 22829 diff changeset	16	\| Act "\<guillemotleft>mvar\<guillemotright>trm" ("Act [_]._" [100,100] 100) (* activate *)
c24395ea4e71 tuned proofs urbanc parents: 22829 diff changeset	17
18106 836135c8acb2 Initial commit. urbanc parents: diff changeset	18
19501 9afa7183dfc2 Capitalized theory names. berghofe parents: 18659 diff changeset	19	end

author	haftmann
	Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744	3daaf23b9ab4
parent 25867	c24395ea4e71
child 41589	bbd861837ebc
permissions	-rw-r--r--