--- a/src/HOL/IMPP/Misc.thy Sat Sep 17 19:17:35 2005 +0200
+++ b/src/HOL/IMPP/Misc.thy Sat Sep 17 20:14:30 2005 +0200
@@ -2,18 +2,22 @@
ID: $Id$
Author: David von Oheimb
Copyright 1999 TUM
+*)
-Several examples for Hoare logic
-*)
-Misc = Hoare +
+header {* Several examples for Hoare logic *}
+
+theory Misc
+imports Hoare
+begin
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)))"
+ 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)))"
+
+ML {* use_legacy_bindings (the_context ()) *}
end
-
\ No newline at end of file