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