30 

    30 

    31 text {* 

    31 text {* 

    32   Sequential composition of two languages @{text "L1"} and @{text "L2"} 

    32   Sequential composition of two languages @{text "L1"} and @{text "L2"} 

    33 *}

    33 *}

    34 

    34 

    36 where 

    37 where 

    37   "A ;; B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"

    38   "A ;; B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"

    38 

    39 

    39 text {* Some properties of operator @{text ";;"}. *}

    40 text {* Some properties of operator @{text ";;"}. *}

    40 

    41