equal
deleted
inserted
replaced
6 Partly from Misra's Chapter 5: Asynchronous Compositions of Programs |
6 Partly from Misra's Chapter 5: Asynchronous Compositions of Programs |
7 *) |
7 *) |
8 |
8 |
9 header{*Unions of Programs*} |
9 header{*Unions of Programs*} |
10 |
10 |
11 theory Union = SubstAx + FP: |
11 theory Union imports SubstAx FP begin |
12 |
12 |
13 constdefs |
13 constdefs |
14 |
14 |
15 (*FIXME: conjoin Init F \<inter> Init G \<noteq> {} *) |
15 (*FIXME: conjoin Init F \<inter> Init G \<noteq> {} *) |
16 ok :: "['a program, 'a program] => bool" (infixl "ok" 65) |
16 ok :: "['a program, 'a program] => bool" (infixl "ok" 65) |