equal
deleted
inserted
replaced
10 translations |
10 translations |
11 "\<lbrace>b\<rbrace>" \<rightharpoonup> "CONST Collect \<guillemotleft>b\<guillemotright>" |
11 "\<lbrace>b\<rbrace>" \<rightharpoonup> "CONST Collect \<guillemotleft>b\<guillemotright>" |
12 |
12 |
13 parse_translation \<open> |
13 parse_translation \<open> |
14 let |
14 let |
15 fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t |
15 fun quote_tr [t] = Syntax_Trans.quote_tr \<^syntax_const>\<open>_antiquote\<close> t |
16 | quote_tr ts = raise TERM ("quote_tr", ts); |
16 | quote_tr ts = raise TERM ("quote_tr", ts); |
17 in [(@{syntax_const "_quote"}, K quote_tr)] end |
17 in [(\<^syntax_const>\<open>_quote\<close>, K quote_tr)] end |
18 \<close> |
18 \<close> |
19 |
19 |
20 end |
20 end |