equal
deleted
inserted
replaced
28 "\<not> s ==> exec (While c) s s" | |
28 "\<not> s ==> exec (While c) s s" | |
29 "s ==> exec c s s' ==> exec (While c) s' s'' ==> exec (While c) s s''" |
29 "s ==> exec c s s' ==> exec (While c) s' s'' ==> exec (While c) s s''" |
30 |
30 |
31 lemma |
31 lemma |
32 "exec c s s' ==> exec (Seq c c) s s'" |
32 "exec c s s' ==> exec (Seq c c) s s'" |
33 quickcheck[generator = predicate_compile_wo_ff, size = 2, iterations = 10] |
33 quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 10] |
34 oops |
34 oops |
35 |
35 |
36 |
36 |
37 end |
37 end |