changeset 58826 | 2ed2eaabe3df |
parent 57948 | 75724d71013c |
child 58889 | 5b7a9633cfa8 |
58825:2065f49da190 | 58826:2ed2eaabe3df |
---|---|
589 val thin_refl = @{thm thin_refl} |
589 val thin_refl = @{thm thin_refl} |
590 ); |
590 ); |
591 open Hypsubst; |
591 open Hypsubst; |
592 *} |
592 *} |
593 |
593 |
594 setup hypsubst_setup |
|
595 ML_file "intprover.ML" |
594 ML_file "intprover.ML" |
596 |
595 |
597 |
596 |
598 subsection {* Intuitionistic Reasoning *} |
597 subsection {* Intuitionistic Reasoning *} |
599 |
598 |