equal
deleted
inserted
replaced
895 \end{rail} |
895 \end{rail} |
896 |
896 |
897 The \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} method solves problems of |
897 The \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} method solves problems of |
898 \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers |
898 \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers |
899 applications in confluence theory, lattice theory and projective |
899 applications in confluence theory, lattice theory and projective |
900 geometry. See \hyperlink{file.~~/src/HOL/ex/Coherent.thy}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}HOL{\isaliteral{2F}{\isacharslash}}ex{\isaliteral{2F}{\isacharslash}}Coherent{\isaliteral{2E}{\isachardot}}thy}}}} for some |
900 geometry. See \verb|~~/src/HOL/ex/Coherent.thy| for some |
901 examples.% |
901 examples.% |
902 \end{isamarkuptext}% |
902 \end{isamarkuptext}% |
903 \isamarkuptrue% |
903 \isamarkuptrue% |
904 % |
904 % |
905 \isamarkupsection{Checking and refuting propositions% |
905 \isamarkupsection{Checking and refuting propositions% |