equal
deleted
inserted
replaced
6 |
6 |
7 theory Correctness |
7 theory Correctness |
8 imports SimCorrectness Spec Impl |
8 imports SimCorrectness Spec Impl |
9 begin |
9 begin |
10 |
10 |
11 defaultsort type |
11 default_sort type |
12 |
12 |
13 definition |
13 definition |
14 sim_relation :: "((nat * bool) * (nat set * bool)) set" where |
14 sim_relation :: "((nat * bool) * (nat set * bool)) set" where |
15 "sim_relation = {qua. let c = fst qua; a = snd qua ; |
15 "sim_relation = {qua. let c = fst qua; a = snd qua ; |
16 k = fst c; b = snd c; |
16 k = fst c; b = snd c; |