equal
deleted
inserted
replaced
4 Copyright 2001 Technische Universitaet Muenchen |
4 Copyright 2001 Technische Universitaet Muenchen |
5 *) |
5 *) |
6 |
6 |
7 header "Equivalence of Operational and Axiomatic Semantics" |
7 header "Equivalence of Operational and Axiomatic Semantics" |
8 |
8 |
9 theory Equivalence = OpSem + AxSem: |
9 theory Equivalence imports OpSem AxSem begin |
10 |
10 |
11 subsection "Validity" |
11 subsection "Validity" |
12 |
12 |
13 constdefs |
13 constdefs |
14 valid :: "[assn,stmt, assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) |
14 valid :: "[assn,stmt, assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) |