equal
deleted
inserted
replaced
345 |
345 |
346 (*****************************************************************************) |
346 (*****************************************************************************) |
347 |
347 |
348 subsubsection {* Schematic variables *} |
348 subsubsection {* Schematic variables *} |
349 |
349 |
350 lemma "?P" |
350 schematic_lemma "?P" |
351 refute |
351 refute |
352 apply auto |
352 apply auto |
353 done |
353 done |
354 |
354 |
355 lemma "x = ?y" |
355 schematic_lemma "x = ?y" |
356 refute |
356 refute |
357 apply auto |
357 apply auto |
358 done |
358 done |
359 |
359 |
360 (******************************************************************************) |
360 (******************************************************************************) |