--- a/src/HOLCF/IOA/Storage/Correctness.thy Sun Oct 21 14:21:45 2007 +0200
+++ b/src/HOLCF/IOA/Storage/Correctness.thy Sun Oct 21 14:21:48 2007 +0200
@@ -11,13 +11,13 @@
defaultsort type
-constdefs
- sim_relation :: "((nat * bool) * (nat set * bool)) set"
- "sim_relation == {qua. let c = fst qua; a = snd qua ;
- k = fst c; b = snd c;
- used = fst a; c = snd a
- in
- (! l:used. l < k) & b=c }"
+definition
+ sim_relation :: "((nat * bool) * (nat set * bool)) set" where
+ "sim_relation = {qua. let c = fst qua; a = snd qua ;
+ k = fst c; b = snd c;
+ used = fst a; c = snd a
+ in
+ (! l:used. l < k) & b=c}"
declare split_paired_All [simp]
declare split_paired_Ex [simp del]