| changeset 13895 | b6105462ccd3 |
| parent 13894 | 8018173a7979 |
| child 13896 | 717bd79b976f |
| 13894:8018173a7979 | 13895:b6105462ccd3 |
|---|---|
1 (* Title: ZF/IMP/Evala0.thy |
|
2 ID: $Id$ |
|
3 Author: Heiko Loetzbeyer & Robert Sandner, TUM |
|
4 Copyright 1994 TUM |
|
5 *) |
|
6 |
|
7 Evala0 = Aexp + |
|
8 |
|
9 consts evala :: "i" |
|
10 "@evala" :: "[i,i,i] => o" ("<_,_>/ -a-> _") |
|
11 |
|
12 translations |
|
13 "<ae,sig> -a-> n" == "<ae,sig,n> : evala" |
|
14 end |