--- a/doc-src/Ref/thm.tex Thu Jul 08 18:26:24 1999 +0200
+++ b/doc-src/Ref/thm.tex Thu Jul 08 18:27:01 1999 +0200
@@ -747,7 +747,8 @@
fail. Isabelle normally builds minimal proof objects, which include only uses
of oracles. You can also request an intermediate level of detail, containing
uses of oracles, axioms and theorems. These smaller proof objects indicate a
-theorem's dependencies.
+theorem's dependencies. Theorems involving oracles will be printed with a
+suffixed \verb|[!]| to point out the different quality of confidence achieved.
Isabelle provides proof objects for the sake of transparency. Their aim is to
increase your confidence in Isabelle. They let you inspect proofs constructed