equal
deleted
inserted
replaced
352 \ --> (ALL x. ALL y. q(x,y) <-> q(y,x))"; |
352 \ --> (ALL x. ALL y. q(x,y) <-> q(y,x))"; |
353 by (mini_tac 1); |
353 by (mini_tac 1); |
354 by (deepen_tac FOL_cs 5 1); |
354 by (deepen_tac FOL_cs 5 1); |
355 (*Faster alternative proof! |
355 (*Faster alternative proof! |
356 by (asm_simp_tac FOL_ss 1); by (fast_tac FOL_cs 1); |
356 by (asm_simp_tac FOL_ss 1); by (fast_tac FOL_cs 1); |
|
357 Can use just deepen_tac but it requires 253 secs?!? |
|
358 by (deepen_tac FOL_cs 0 1); |
357 *) |
359 *) |
358 result(); |
360 result(); |
359 |
361 |
360 writeln"Problem 44"; |
362 writeln"Problem 44"; |
361 goal FOL.thy "(ALL x. f(x) --> \ |
363 goal FOL.thy "(ALL x. f(x) --> \ |