equal
deleted
inserted
replaced
188 "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g" |
188 "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g" |
189 (* quickcheck[exhaustive, size = 9, timeout = 2000] -- maybe possible with a lot of time *) |
189 (* quickcheck[exhaustive, size = 9, timeout = 2000] -- maybe possible with a lot of time *) |
190 quickcheck[narrowing, size = 7, expect = counterexample] |
190 quickcheck[narrowing, size = 7, expect = counterexample] |
191 oops |
191 oops |
192 |
192 |
193 ebd |
193 end |