src/HOL/Typerep.thy
changeset 80760 be8c0e039a5e
parent 74375 ba880f3a4e52
child 80932 261cd8722677
--- a/src/HOL/Typerep.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/Typerep.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -19,6 +19,8 @@
 
 syntax
   "_TYPEREP" :: "type => logic"  ("(1TYPEREP/(1'(_')))")
+syntax_consts
+  "_TYPEREP" \<rightleftharpoons> typerep
 
 parse_translation \<open>
   let