src/HOL/IMPP/Misc.thy
 changeset 17477 ceb42ea2f223 parent 8177 e59e93ad85eb child 19803 aa2581752afb
equal inserted replaced
17476:315cb57e3dd7 17477:ceb42ea2f223
`     1 (*  Title:      HOL/IMPP/Misc.thy`
`     1 (*  Title:      HOL/IMPP/Misc.thy`
`     2     ID:         \$Id\$`
`     2     ID:         \$Id\$`
`     3     Author:     David von Oheimb`
`     3     Author:     David von Oheimb`
`     4     Copyright   1999 TUM`
`     4     Copyright   1999 TUM`
`       `
`     5 *)`
`     5 `
`     6 `
`     6 Several examples for Hoare logic`
`     7 header {* Several examples for Hoare logic *}`
`     7 *)`
`     8 `
`     8 Misc = Hoare +`
`     9 theory Misc`
`       `
`    10 imports Hoare`
`       `
`    11 begin`
`     9 `
`    12 `
`    10 defs`
`    13 defs`
`    11   newlocs_def "newlocs       == %x. arbitrary"`
`    14   newlocs_def: "newlocs       == %x. arbitrary"`
`    12   setlocs_def "setlocs s l'  == case s of st g l => st g l'"`
`    15   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"`
`    16   getlocs_def: "getlocs s     == case s of st g l => l"`
`    14    update_def "update s vn v == case vn of`
`    17    update_def: "update s vn v == case vn of`
`    15                               Glb gn => (case s of st g l => st (g(gn:=v)) l)`
`    18                                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)))"`
`    19                              | Loc ln => (case s of st g l => st g (l(ln:=v)))"`
`       `
`    20 `
`       `
`    21 ML {* use_legacy_bindings (the_context ()) *}`
`    17 `
`    22 `
`    18 end`
`    23 end`