changeset 81125 | ec121999a9cb |
parent 80934 | 8e72f55295fd |
child 81507 | 08574da77b4a |
--- a/src/HOL/Typerep.thy Sun Oct 06 22:56:07 2024 +0200 +++ b/src/HOL/Typerep.thy Tue Oct 08 12:10:35 2024 +0200 @@ -18,7 +18,7 @@ end syntax - "_TYPEREP" :: "type => logic" (\<open>(\<open>indent=1 notation=\<open>prefix TYPEREP\<close>\<close>TYPEREP/(1'(_')))\<close>) + "_TYPEREP" :: "type => logic" (\<open>(\<open>indent=1 notation=\<open>mixfix TYPEREP\<close>\<close>TYPEREP/(1'(_')))\<close>) syntax_consts "_TYPEREP" \<rightleftharpoons> typerep