src/HOL/IMPP/Misc.thy
changeset 8177 e59e93ad85eb
child 17477 ceb42ea2f223
equal deleted inserted replaced
8176:db112d36a426 8177:e59e93ad85eb
       
     1 (*  Title:      HOL/IMPP/Misc.thy
       
     2     ID:         $Id$
       
     3     Author:     David von Oheimb
       
     4     Copyright   1999 TUM
       
     5 
       
     6 Several examples for Hoare logic
       
     7 *)
       
     8 Misc = Hoare +
       
     9 
       
    10 defs
       
    11   newlocs_def "newlocs       == %x. arbitrary"
       
    12   setlocs_def "setlocs s l'  == case s of st g l => st g l'"
       
    13   getlocs_def "getlocs s     == case s of st g l => l"
       
    14    update_def "update s vn v == case vn of
       
    15                               Glb gn => (case s of st g l => st (g(gn:=v)) l)
       
    16                             | Loc ln => (case s of st g l => st g (l(ln:=v)))"
       
    17 
       
    18 end
       
    19