1structure alignmentSyntax :> alignmentSyntax =
2struct
3
4open Abbrev HolKernel alignmentTheory
5
6val s = HolKernel.syntax_fns1 "alignment"
7val (byte_align_tm, mk_byte_align, dest_byte_align, is_byte_align) =
8   s "byte_align"
9val (byte_aligned_tm, mk_byte_aligned, dest_byte_aligned, is_byte_aligned) =
10   s "byte_aligned"
11
12val s = HolKernel.syntax_fns2 "alignment"
13val (align_tm, mk_align, dest_align, is_align) = s "align"
14val (aligned_tm, mk_aligned, dest_aligned, is_aligned) = s "aligned"
15
16end
17