| author | paulson |
| Wed, 25 Nov 1998 15:54:41 +0100 | |
| changeset 5971 | c5a7a7685826 |
| parent 482 | 3a4e092ba69c |
| permissions | -rw-r--r-- |
| 482 | 1 |
(* Title: ZF/IMP/Evalc0.thy |
2 |
ID: $Id$ |
|
3 |
Author: Heiko Loetzbeyer & Robert Sandner, TUM |
|
4 |
Copyright 1994 TUM |
|
5 |
*) |
|
6 |
||
7 |
Evalc0 = Evalb + Com + Assign + |
|
8 |
||
9 |
consts |
|
10 |
evalc :: "i" |
|
11 |
"@evalc" :: "[i,i,i] => o" ("<_,_>/ -c-> _")
|
|
12 |
||
13 |
translations |
|
14 |
"<ce,sig> -c-> s" == "<ce,sig,s> : evalc" |
|
15 |
end |