author | nipkow |
Mon, 29 Nov 2004 11:23:48 +0100 | |
changeset 15339 | a7b603bbc1e6 |
parent 8177 | e59e93ad85eb |
child 17477 | ceb42ea2f223 |
permissions | -rw-r--r-- |
(* Title: HOL/IMPP/Misc.thy ID: $Id$ Author: David von Oheimb Copyright 1999 TUM Several examples for Hoare logic *) Misc = Hoare + defs newlocs_def "newlocs == %x. arbitrary" setlocs_def "setlocs s l' == case s of st g l => st g l'" getlocs_def "getlocs s == case s of st g l => l" update_def "update s vn v == case vn of Glb gn => (case s of st g l => st (g(gn:=v)) l) | Loc ln => (case s of st g l => st g (l(ln:=v)))" end