equal
deleted
inserted
replaced
840 The corresponding ML-code is as follows:\footnote{Note that @{text "|>"} is reverse |
840 The corresponding ML-code is as follows:\footnote{Note that @{text "|>"} is reverse |
841 application. See Section~\ref{sec:combinators}.} |
841 application. See Section~\ref{sec:combinators}.} |
842 |
842 |
843 @{ML_response_fake [display,gray] |
843 @{ML_response_fake [display,gray] |
844 "let |
844 "let |
845 val thy = @{theory} |
845 |
846 |
846 val assm1 = @{cprop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"} |
847 val assm1 = cterm_of thy @{prop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"} |
847 val assm2 = @{cprop \"(P::nat\<Rightarrow>bool) t\"} |
848 val assm2 = cterm_of thy @{prop \"(P::nat\<Rightarrow>bool) t\"} |
|
849 |
848 |
850 val Pt_implies_Qt = |
849 val Pt_implies_Qt = |
851 assume assm1 |
850 assume assm1 |
852 |> forall_elim (cterm_of thy @{term \"t::nat\"}); |
851 |> forall_elim @{cterm \"t::nat\"}; |
853 |
852 |
854 val Qt = implies_elim Pt_implies_Qt (assume assm2); |
853 val Qt = implies_elim Pt_implies_Qt (assume assm2); |
855 in |
854 in |
856 Qt |
855 Qt |
857 |> implies_intr assm2 |
856 |> implies_intr assm2 |