diff -r a0189ff58b7c -r 24ec32bee347 src/HOLCF/IOA/Storage/Impl.thy
--- a/src/HOLCF/IOA/Storage/Impl.thy	Wed Jun 25 18:23:50 2008 +0200
+++ b/src/HOLCF/IOA/Storage/Impl.thy	Wed Jun 25 21:25:51 2008 +0200
@@ -9,34 +9,32 @@
 imports IOA Action
 begin
 
-consts
-
-impl_sig   :: "action signature"
-impl_trans :: "(action, nat  * bool)transition set"
-impl_ioa   :: "(action, nat * bool)ioa"
-
-defs
-
-sig_def: "impl_sig == (UN l.{Free l} Un {New},
-                     UN l.{Loc l},
-                     {})"
+definition
+  impl_sig :: "action signature" where
+  "impl_sig = (UN l.{Free l} Un {New},
+               UN l.{Loc l},
+               {})"
 
-trans_def: "impl_trans ==
- {tr. let s = fst(tr); k = fst s; b = snd s;
-          t = snd(snd(tr)); k' = fst t; b' = snd t
-      in
-      case fst(snd(tr))
-      of
-      New       => k' = k & b'  |
-      Loc l     => b & l= k & k'= (Suc k) & ~b' |
-      Free l    => k'=k & b'=b}"
+definition
+  impl_trans :: "(action, nat  * bool)transition set" where
+  "impl_trans =
+    {tr. let s = fst(tr); k = fst s; b = snd s;
+             t = snd(snd(tr)); k' = fst t; b' = snd t
+         in
+         case fst(snd(tr))
+         of
+         New       => k' = k & b'  |
+         Loc l     => b & l= k & k'= (Suc k) & ~b' |
+         Free l    => k'=k & b'=b}"
 
-ioa_def: "impl_ioa == (impl_sig, {(0,False)}, impl_trans,{},{})"
+definition
+  impl_ioa :: "(action, nat * bool)ioa" where
+  "impl_ioa = (impl_sig, {(0,False)}, impl_trans,{},{})"
 
 lemma in_impl_asig:
   "New : actions(impl_sig) &
     Loc l : actions(impl_sig) &
     Free l : actions(impl_sig) "
-  by (simp add: Impl.sig_def actions_def asig_projections)
+  by (simp add: impl_sig_def actions_def asig_projections)
 
 end