| changeset 16417 | 9bc16273c2d4 |
| parent 14141 | d3916d9183d2 |
| child 22271 | 51a80e238b29 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
4 Copyright 1999 Technische Universitaet Muenchen |
4 Copyright 1999 Technische Universitaet Muenchen |
5 *) |
5 *) |
6 |
6 |
7 header {* \isaheader{Operational Evaluation (big step) Semantics} *} |
7 header {* \isaheader{Operational Evaluation (big step) Semantics} *} |
8 |
8 |
9 theory Eval = State + WellType: |
9 theory Eval imports State WellType begin |
10 |
10 |
11 |
11 |
12 -- "Auxiliary notions" |
12 -- "Auxiliary notions" |
13 |
13 |
14 constdefs |
14 constdefs |