equal
deleted
inserted
replaced
1 (* Title: HOL/UNITY/Update.thy |
1 (* Title: HOL/Update.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1998 University of Cambridge |
4 Copyright 1998 University of Cambridge |
5 |
5 |
6 Function updates: like the standard theory Map, but for ordinary functions |
6 Function updates: like theory Map, but for ordinary functions |
7 *) |
7 *) |
8 |
8 |
9 open Update; |
9 open Update; |
10 |
10 |
11 goalw thy [update_def] "(f[x:=y] = f) = (f x = y)"; |
11 goalw thy [update_def] "(f[x:=y] = f) = (f x = y)"; |