equal
deleted
inserted
replaced
262 by (Int.best_tac 1); |
262 by (Int.best_tac 1); |
263 result(); |
263 result(); |
264 |
264 |
265 writeln"Problem 24"; |
265 writeln"Problem 24"; |
266 goal IFOLP.thy "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & \ |
266 goal IFOLP.thy "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & \ |
267 \ ~(EX x.P(x)) --> (EX x.Q(x)) & (ALL x. Q(x)|R(x) --> S(x)) \ |
267 \ (~(EX x.P(x)) --> (EX x.Q(x))) & (ALL x. Q(x)|R(x) --> S(x)) \ |
268 \ --> (EX x. P(x)&R(x))"; |
268 \ --> ~~(EX x. P(x)&R(x))"; |
|
269 (*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*) |
|
270 by Int.safe_tac; |
|
271 by (etac impE 1); |
|
272 by (Int.fast_tac 1); |
269 by (Int.fast_tac 1); |
273 by (Int.fast_tac 1); |
270 result(); |
274 result(); |
271 |
275 |
272 writeln"Problem 25"; |
276 writeln"Problem 25"; |
273 goal IFOLP.thy "?p : (EX x. P(x)) & \ |
277 goal IFOLP.thy "?p : (EX x. P(x)) & \ |