# HG changeset patch
# User wenzelm
# Date 931451221 -7200
# Node ID 7e166f8d412e144d7dff88f935afb574b355e891
# Parent  51c415f15007b7f97674ca143ef0c5f644688140
Theorems involving oracles will be printed with a suffixed \verb|[!]|;

diff -r 51c415f15007 -r 7e166f8d412e doc-src/Ref/thm.tex
--- 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