--- a/src/HOLCF/IOA/Storage/Spec.thy Sat Sep 03 16:49:48 2005 +0200
+++ b/src/HOLCF/IOA/Storage/Spec.thy Sat Sep 03 16:50:22 2005 +0200
@@ -1,12 +1,13 @@
(* Title: HOL/IOA/example/Spec.thy
ID: $Id$
Author: Olaf Müller
-
-The specification of a memory.
*)
-Spec = IOA + Action +
+header {* The specification of a memory *}
+theory Spec
+imports IOA Action
+begin
consts
@@ -16,20 +17,22 @@
defs
-sig_def "spec_sig == (UN l.{Free l} Un {New},
- UN l.{Loc l},
+sig_def: "spec_sig == (UN l.{Free l} Un {New},
+ UN l.{Loc l},
{})"
-trans_def "spec_trans ==
- {tr. let s = fst(tr); used = fst s; c = snd s;
- t = snd(snd(tr)); used' = fst t; c' = snd t
- in
- case fst(snd(tr))
- of
- New => used' = used & c' |
- Loc l => c & l~:used & used'= used Un {l} & ~c' |
+trans_def: "spec_trans ==
+ {tr. let s = fst(tr); used = fst s; c = snd s;
+ t = snd(snd(tr)); used' = fst t; c' = snd t
+ in
+ case fst(snd(tr))
+ of
+ New => used' = used & c' |
+ Loc l => c & l~:used & used'= used Un {l} & ~c' |
Free l => used'=used - {l} & c'=c}"
-ioa_def "spec_ioa == (spec_sig, {({},False)}, spec_trans,{},{})"
+ioa_def: "spec_ioa == (spec_sig, {({},False)}, spec_trans,{},{})"
+
+ML {* use_legacy_bindings (the_context ()) *}
end