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

19501 9afa7183dfc2 Capitalized theory names. berghofe parents: 18659 diff changeset	1	theory Lambda_mu
66453 cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 63167 diff changeset	2	imports "HOL-Nominal.Nominal"
18106 836135c8acb2 Initial commit. urbanc parents: diff changeset	3	begin
836135c8acb2 Initial commit. urbanc parents: diff changeset	4
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 41589 diff changeset	5	section \<open>Lambda-Mu according to a paper by Gavin Bierman\<close>
18106 836135c8acb2 Initial commit. urbanc parents: diff changeset	6
836135c8acb2 Initial commit. urbanc parents: diff changeset	7	atom_decl var mvar
836135c8acb2 Initial commit. urbanc parents: diff changeset	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"
80914 d97fdabd9e2b standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing; wenzelm parents: 66453 diff changeset	11	\| Lam "\<guillemotleft>var\<guillemotright>trm" (\<open>Lam [_]._\<close> [100,100] 100)
22829 f1db55c7534d tuned some proofs and changed variable names in some definitions of Nominal.thy urbanc parents: 19501 diff changeset	12	\| App "trm" "trm"
25867 c24395ea4e71 tuned proofs urbanc parents: 22829 diff changeset	13	\| Pss "mvar" "trm" (* passivate *)
80914 d97fdabd9e2b standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing; wenzelm parents: 66453 diff changeset	14	\| Act "\<guillemotleft>mvar\<guillemotright>trm" (\<open>Act [_]._\<close> [100,100] 100) (* activate *)
25867 c24395ea4e71 tuned proofs urbanc parents: 22829 diff changeset	15
18106 836135c8acb2 Initial commit. urbanc parents: diff changeset	16
19501 9afa7183dfc2 Capitalized theory names. berghofe parents: 18659 diff changeset	17	end

author	wenzelm
	Wed, 25 Jun 2025 16:35:25 +0200
changeset 82768	8f866fd6fae1
parent 80914	d97fdabd9e2b
permissions	-rw-r--r--