summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 08 Jul 1999 18:27:01 +0200 | |

changeset 6924 | 7e166f8d412e |

parent 6923 | 51c415f15007 |

child 6925 | 8d4d45ec6a3d |

Theorems involving oracles will be printed with a suffixed \verb|[!]|;

--- 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