| changeset 80754 | 701912f5645a |
| parent 78791 | 4f7dce5c1a81 |
| child 80761 | bc936d3d8b45 |
--- a/src/ZF/Bin.thy Fri Aug 23 22:47:51 2024 +0200 +++ b/src/ZF/Bin.thy Fri Aug 23 23:14:39 2024 +0200 @@ -119,6 +119,8 @@ ML_file \<open>Tools/numeral_syntax.ML\<close> +syntax_consts + "_Int0" "_Int1" "_Int2" "_Int" "_Neg_Int1" "_Neg_Int2" "_Neg_Int" \<rightleftharpoons> integ_of declare bin.intros [simp,TC]