416 text_raw \<open>\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
416 text_raw \<open>\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
417 |
417 |
418 have "A \<longrightarrow> B" |
418 have "A \<longrightarrow> B" |
419 proof |
419 proof |
420 assume A |
420 assume A |
421 show B sorry %noproof |
421 show B \<proof> |
422 qed |
422 qed |
423 |
423 |
424 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
424 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
425 |
425 |
426 have "A \<longrightarrow> B" and A sorry %noproof |
426 have "A \<longrightarrow> B" and A \<proof> |
427 then have B .. |
427 then have B .. |
428 |
428 |
429 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
429 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
430 |
430 |
431 have A sorry %noproof |
431 have A \<proof> |
432 then have "A \<or> B" .. |
432 then have "A \<or> B" .. |
433 |
433 |
434 have B sorry %noproof |
434 have B \<proof> |
435 then have "A \<or> B" .. |
435 then have "A \<or> B" .. |
436 |
436 |
437 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
437 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
438 |
438 |
439 have "A \<or> B" sorry %noproof |
439 have "A \<or> B" \<proof> |
440 then have C |
440 then have C |
441 proof |
441 proof |
442 assume A |
442 assume A |
443 then show C sorry %noproof |
443 then show C \<proof> |
444 next |
444 next |
445 assume B |
445 assume B |
446 then show C sorry %noproof |
446 then show C \<proof> |
447 qed |
447 qed |
448 |
448 |
449 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
449 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
450 |
450 |
451 have A and B sorry %noproof |
451 have A and B \<proof> |
452 then have "A \<and> B" .. |
452 then have "A \<and> B" .. |
453 |
453 |
454 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
454 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
455 |
455 |
456 have "A \<and> B" sorry %noproof |
456 have "A \<and> B" \<proof> |
457 then obtain A and B .. |
457 then obtain A and B .. |
458 |
458 |
459 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
459 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
460 |
460 |
461 have "\<bottom>" sorry %noproof |
461 have "\<bottom>" \<proof> |
462 then have A .. |
462 then have A .. |
463 |
463 |
464 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
464 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
465 |
465 |
466 have "\<top>" .. |
466 have "\<top>" .. |
468 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
468 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
469 |
469 |
470 have "\<not> A" |
470 have "\<not> A" |
471 proof |
471 proof |
472 assume A |
472 assume A |
473 then show "\<bottom>" sorry %noproof |
473 then show "\<bottom>" \<proof> |
474 qed |
474 qed |
475 |
475 |
476 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
476 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
477 |
477 |
478 have "\<not> A" and A sorry %noproof |
478 have "\<not> A" and A \<proof> |
479 then have B .. |
479 then have B .. |
480 |
480 |
481 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
481 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
482 |
482 |
483 have "\<forall>x. B x" |
483 have "\<forall>x. B x" |
484 proof |
484 proof |
485 fix x |
485 fix x |
486 show "B x" sorry %noproof |
486 show "B x" \<proof> |
487 qed |
487 qed |
488 |
488 |
489 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
489 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
490 |
490 |
491 have "\<forall>x. B x" sorry %noproof |
491 have "\<forall>x. B x" \<proof> |
492 then have "B a" .. |
492 then have "B a" .. |
493 |
493 |
494 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
494 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
495 |
495 |
496 have "\<exists>x. B x" |
496 have "\<exists>x. B x" |
497 proof |
497 proof |
498 show "B a" sorry %noproof |
498 show "B a" \<proof> |
499 qed |
499 qed |
500 |
500 |
501 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
501 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
502 |
502 |
503 have "\<exists>x. B x" sorry %noproof |
503 have "\<exists>x. B x" \<proof> |
504 then obtain a where "B a" .. |
504 then obtain a where "B a" .. |
505 |
505 |
506 text_raw \<open>\end{minipage}\<close> |
506 text_raw \<open>\end{minipage}\<close> |
507 |
507 |
508 (*<*) |
508 (*<*) |