src/HOL/Predicate_Compile_Examples/IMP_1.thy
changeset 42031 2de57cda5b24
parent 41413 64cd30d6b0b8
child 42397 13798dcbdca5
equal deleted inserted replaced
42030:96327c909389 42031:2de57cda5b24
     6 
     6 
     7 text {*
     7 text {*
     8   In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, and IF.
     8   In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, and IF.
     9 *}
     9 *}
    10 
    10 
    11 types
    11 type_synonym var = unit
    12   var = unit
    12 type_synonym state = bool
    13   state = bool
       
    14 
    13 
    15 datatype com =
    14 datatype com =
    16   Skip |
    15   Skip |
    17   Ass bool |
    16   Ass bool |
    18   Seq com com |
    17   Seq com com |