isabelle: src/HOL/Hoare_Parallel/Quote_Antiquote.thy@b51e4a526897 (annotated)

59189 ad8e0a789af6 update_cartouches; wenzelm parents: 58884 diff changeset	1	section \<open>Concrete Syntax\<close>
13020 791e3b4c4039 HoareParallel Theories prensani parents: diff changeset	2
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 13020 diff changeset	3	theory Quote_Antiquote imports Main begin
13020 791e3b4c4039 HoareParallel Theories prensani parents: diff changeset	4
791e3b4c4039 HoareParallel Theories prensani parents: diff changeset	5	syntax
80914 d97fdabd9e2b standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing; wenzelm parents: 69597 diff changeset	6	"_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)" (\<open>(\<guillemotleft>_\<guillemotright>)\<close> [0] 1000)
d97fdabd9e2b standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing; wenzelm parents: 69597 diff changeset	7	"_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b" (\<open>\<acute>_\<close> [1000] 1000)
d97fdabd9e2b standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing; wenzelm parents: 69597 diff changeset	8	"_Assert" :: "'a \<Rightarrow> 'a set" (\<open>(\<lbrace>_\<rbrace>)\<close> [0] 1000)
13020 791e3b4c4039 HoareParallel Theories prensani parents: diff changeset	9
791e3b4c4039 HoareParallel Theories prensani parents: diff changeset	10	translations
53241 effd8fcabca2 more symbols; wenzelm parents: 52143 diff changeset	11	"\<lbrace>b\<rbrace>" \<rightharpoonup> "CONST Collect \<guillemotleft>b\<guillemotright>"
13020 791e3b4c4039 HoareParallel Theories prensani parents: diff changeset	12
59189 ad8e0a789af6 update_cartouches; wenzelm parents: 58884 diff changeset	13	parse_translation \<open>
13020 791e3b4c4039 HoareParallel Theories prensani parents: diff changeset	14	let
69597 ff784d5a5bfb isabelle update -u control_cartouches; wenzelm parents: 62390 diff changeset	15	fun quote_tr [t] = Syntax_Trans.quote_tr \<^syntax_const>\<open>_antiquote\<close> t
13020 791e3b4c4039 HoareParallel Theories prensani parents: diff changeset	16	\| quote_tr ts = raise TERM ("quote_tr", ts);
69597 ff784d5a5bfb isabelle update -u control_cartouches; wenzelm parents: 62390 diff changeset	17	in [(\<^syntax_const>\<open>_quote\<close>, K quote_tr)] end
59189 ad8e0a789af6 update_cartouches; wenzelm parents: 58884 diff changeset	18	\<close>
13020 791e3b4c4039 HoareParallel Theories prensani parents: diff changeset	19
62390 842917225d56 more canonical names nipkow parents: 59189 diff changeset	20	end

author	wenzelm
	Mon, 27 Oct 2025 15:16:32 +0100
changeset 83417	b51e4a526897
parent 80914	d97fdabd9e2b
permissions	-rw-r--r--