src/HOLCF/IOA/NTP/Correctness.thy
changeset 25131 2c8caac48ade
parent 19739 c58ef2aa5430
child 26339 7825c83c9eff
--- a/src/HOLCF/IOA/NTP/Correctness.thy	Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/NTP/Correctness.thy	Sun Oct 21 14:21:48 2007 +0200
@@ -9,10 +9,10 @@
 imports Impl Spec
 begin
 
-constdefs
-  hom :: "'m impl_state => 'm list"
-  "hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
-                           else tl(sq(sen s)))"
+definition
+  hom :: "'m impl_state => 'm list" where
+  "hom s = rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
+                         else tl(sq(sen s)))"
 
 ML_setup {*
 (* repeated from Traces.ML *)