--- a/doc-src/IsarImplementation/Thy/document/prelim.tex Fri Aug 03 16:28:15 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Fri Aug 03 16:28:17 2007 +0200
@@ -181,8 +181,8 @@
\end{mldecls}
\begin{mldecls}
\indexmltype{theory-ref}\verb|type theory_ref| \\
- \indexml{Theory.self-ref}\verb|Theory.self_ref: theory -> theory_ref| \\
\indexml{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
+ \indexml{Theory.check-thy}\verb|Theory.check_thy: theory -> theory_ref| \\
\end{mldecls}
\begin{description}
@@ -211,8 +211,10 @@
always valid theory; updates on the original are propagated
automatically.
- \item \verb|Theory.self_ref|~\isa{thy} and \verb|Theory.deref|~\isa{thy{\isacharunderscore}ref} convert between \verb|theory| and \verb|theory_ref|. As the referenced theory
- evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to a larger context.
+ \item \verb|Theory.deref|~\isa{thy{\isacharunderscore}ref} turns a \verb|theory_ref| into an \verb|theory| value. As the referenced
+ theory evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to a larger context.
+
+ \item \verb|Theory.check_thy|~\isa{thy} produces a \verb|theory_ref| from a valid \verb|theory| value.
\end{description}%
\end{isamarkuptext}%
--- a/src/Tools/Metis/metis.ML Fri Aug 03 16:28:15 2007 +0200
+++ b/src/Tools/Metis/metis.ML Fri Aug 03 16:28:17 2007 +0200
@@ -5386,7 +5386,7 @@
| range NONE (SOME j) = "{n IN Z | n <= " ^ Int.toString j ^ "}"
| range (SOME i) (SOME j) =
"{n IN Z | " ^ Int.toString i ^ " <= n <= " ^ Int.toString j ^ "}";
- fun oLeq (SOME (x:int)) (SOME y) = x <= y | oLeq _ _ = true;
+ fun oLeq (SOME (x: int)) (SOME y) = x <= y | oLeq _ _ = true;
fun argToInt arg omin omax x =
(case Int.fromString x of
SOME i =>