src/HOL/Hoare_Parallel/OG_Com.thy
changeset 42174 d0be2722ce9f
parent 39246 9e58f0499f57
child 58249 180f1b3508ed
equal deleted inserted replaced
42173:5d33c12ccf22 42174:d0be2722ce9f
     5 
     5 
     6 theory OG_Com imports Main begin
     6 theory OG_Com imports Main begin
     7 
     7 
     8 text {* Type abbreviations for boolean expressions and assertions: *}
     8 text {* Type abbreviations for boolean expressions and assertions: *}
     9 
     9 
    10 types
    10 type_synonym 'a bexp = "'a set"
    11     'a bexp = "'a set"
    11 type_synonym 'a assn = "'a set"
    12     'a assn = "'a set"
       
    13 
    12 
    14 text {* The syntax of commands is defined by two mutually recursive
    13 text {* The syntax of commands is defined by two mutually recursive
    15 datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a
    14 datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a
    16 com"} for non-annotated commands. *}
    15 com"} for non-annotated commands. *}
    17 
    16