changeset 80934 | 8e72f55295fd |
parent 80932 | 261cd8722677 |
child 81125 | ec121999a9cb |
--- a/src/HOL/Typerep.thy Mon Sep 23 15:01:10 2024 +0200 +++ b/src/HOL/Typerep.thy Mon Sep 23 21:09:23 2024 +0200 @@ -18,7 +18,7 @@ end syntax - "_TYPEREP" :: "type => logic" (\<open>(1TYPEREP/(1'(_')))\<close>) + "_TYPEREP" :: "type => logic" (\<open>(\<open>indent=1 notation=\<open>prefix TYPEREP\<close>\<close>TYPEREP/(1'(_')))\<close>) syntax_consts "_TYPEREP" \<rightleftharpoons> typerep