equal
deleted
inserted
replaced
330 |
330 |
331 (*****************************************************************************) |
331 (*****************************************************************************) |
332 |
332 |
333 subsubsection {* Schematic variables *} |
333 subsubsection {* Schematic variables *} |
334 |
334 |
335 schematic_lemma "?P" |
335 schematic_goal "?P" |
336 refute [expect = none] |
336 refute [expect = none] |
337 by auto |
337 by auto |
338 |
338 |
339 schematic_lemma "x = ?y" |
339 schematic_goal "x = ?y" |
340 refute [expect = none] |
340 refute [expect = none] |
341 by auto |
341 by auto |
342 |
342 |
343 (******************************************************************************) |
343 (******************************************************************************) |
344 |
344 |