equal
deleted
inserted
replaced
1 (* Title: HOL/MicroJava/J/Eval.thy |
1 (* Title: HOL/MicroJava/J/Eval.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: David von Oheimb |
3 Author: David von Oheimb |
4 Copyright 1999 Technische Universitaet Muenchen |
4 Copyright 1999 Technische Universitaet Muenchen |
|
5 *) |
5 |
6 |
6 Operational evaluation (big-step) semantics of the |
7 header "Operational Evaluation (big-step) Semantics" |
7 execution of Java expressions and statements |
|
8 *) |
|
9 |
8 |
10 theory Eval = State + WellType: |
9 theory Eval = State + WellType: |
11 |
10 |
12 consts |
11 consts |
13 eval :: "java_mb prog => (xstate \<times> expr \<times> val \<times> xstate) set" |
12 eval :: "java_mb prog => (xstate \<times> expr \<times> val \<times> xstate) set" |