changeset 13895 | b6105462ccd3 |
parent 13894 | 8018173a7979 |
child 13896 | 717bd79b976f |
13894:8018173a7979 | 13895:b6105462ccd3 |
---|---|
1 (* Title: ZF/IMP/Assign.thy |
|
2 ID: $Id$ |
|
3 Author: Heiko Loetzbeyer & Robert Sandner, TUM |
|
4 Copyright 1994 TUM |
|
5 *) |
|
6 |
|
7 Assign = Aexp + |
|
8 consts |
|
9 "assign" :: "[i,i,i] => i" ("_[_'/_]" [900,0,0] 900) |
|
10 |
|
11 rules |
|
12 assign_def "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)" |
|
13 end |