710 \begin{mldecls} |
710 \begin{mldecls} |
711 \indexdef{}{ML type}{ctyp}\verb|type ctyp| \\ |
711 \indexdef{}{ML type}{ctyp}\verb|type ctyp| \\ |
712 \indexdef{}{ML type}{cterm}\verb|type cterm| \\ |
712 \indexdef{}{ML type}{cterm}\verb|type cterm| \\ |
713 \indexdef{}{ML}{Thm.ctyp\_of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\ |
713 \indexdef{}{ML}{Thm.ctyp\_of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\ |
714 \indexdef{}{ML}{Thm.cterm\_of}\verb|Thm.cterm_of: theory -> term -> cterm| \\ |
714 \indexdef{}{ML}{Thm.cterm\_of}\verb|Thm.cterm_of: theory -> term -> cterm| \\ |
715 \indexdef{}{ML}{Thm.capply}\verb|Thm.capply: cterm -> cterm -> cterm| \\ |
715 \indexdef{}{ML}{Thm.apply}\verb|Thm.apply: cterm -> cterm -> cterm| \\ |
716 \indexdef{}{ML}{Thm.cabs}\verb|Thm.cabs: cterm -> cterm -> cterm| \\ |
716 \indexdef{}{ML}{Thm.lambda}\verb|Thm.lambda: cterm -> cterm -> cterm| \\ |
717 \indexdef{}{ML}{Thm.all}\verb|Thm.all: cterm -> cterm -> cterm| \\ |
717 \indexdef{}{ML}{Thm.all}\verb|Thm.all: cterm -> cterm -> cterm| \\ |
718 \indexdef{}{ML}{Drule.mk\_implies}\verb|Drule.mk_implies: cterm * cterm -> cterm| \\ |
718 \indexdef{}{ML}{Drule.mk\_implies}\verb|Drule.mk_implies: cterm * cterm -> cterm| \\ |
719 \end{mldecls} |
719 \end{mldecls} |
720 \begin{mldecls} |
720 \begin{mldecls} |
721 \indexdef{}{ML type}{thm}\verb|type thm| \\ |
721 \indexdef{}{ML type}{thm}\verb|type thm| \\ |
765 respectively. This also involves some basic normalizations, such |
765 respectively. This also involves some basic normalizations, such |
766 expansion of type and term abbreviations from the theory context. |
766 expansion of type and term abbreviations from the theory context. |
767 Full re-certification is relatively slow and should be avoided in |
767 Full re-certification is relatively slow and should be avoided in |
768 tight reasoning loops. |
768 tight reasoning loops. |
769 |
769 |
770 \item \verb|Thm.capply|, \verb|Thm.cabs|, \verb|Thm.all|, \verb|Drule.mk_implies| etc.\ compose certified terms (or propositions) |
770 \item \verb|Thm.apply|, \verb|Thm.lambda|, \verb|Thm.all|, \verb|Drule.mk_implies| etc.\ compose certified terms (or propositions) |
771 incrementally. This is equivalent to \verb|Thm.cterm_of| after |
771 incrementally. This is equivalent to \verb|Thm.cterm_of| after |
772 unchecked \verb|$|, \verb|lambda|, \verb|Logic.all|, \verb|Logic.mk_implies| etc., but there can be a big difference in |
772 unchecked \verb|$|, \verb|lambda|, \verb|Logic.all|, \verb|Logic.mk_implies| etc., but there can be a big difference in |
773 performance when large existing entities are composed by a few extra |
773 performance when large existing entities are composed by a few extra |
774 constructions on top. There are separate operations to decompose |
774 constructions on top. There are separate operations to decompose |
775 certified terms and theorems to produce certified terms again. |
775 certified terms and theorems to produce certified terms again. |