lib/Tools/doc

Prototype introiff option for find_theorems.

This feature was suggested by Jeremy Avigad / Tobias Nipkow.

It adds an introiff keyword for find_theorems that returns, in
addition to the usual results for intro, any theorems of the
form ([| ... |] ==> (P = Q)) where either P or Q matches the
conclusions of the current goal. Such theorems can be made
introduction rules with [THEN iffDx].

The current patch is for evaluation only. It assumes an
(op = : 'a -> 'a -> bool) operator, which is specific to HOL.
It is not clear how this should be generalised.

+
−#!/usr/bin/env bash
+
−#
+
−# Author: Markus Wenzel, TU Muenchen
+
−#
+
−# DESCRIPTION: view Isabelle documentation
+
−
+
−
+
−PRG="$(basename "$0")"
+
−
+
−function usage()
+
−{
+
−  echo
+
−  echo "Usage: isabelle $PRG [DOC]"
+
−  echo
+
−  echo "  View Isabelle documentation DOC, or show list of available documents."
+
−  echo
+
−  exit 1
+
−}
+
−
+
−function fail()
+
−{
+
−  echo "$1" >&2
+
−  exit 2
+
−}
+
−
+
−
+
−## args
+
−
+
−DOC=""
+
−[ "$#" -ge 1 ] && { DOC="$1"; shift; }
+
−
+
−[ "$#" -ne 0 -o "$DOC" = "-?" ] && usage
+
−
+
−
+
−## main
+
−
+
−if [ -z "$DOC" ]; then
+
−  ORIG_IFS="$IFS"
+
−  IFS=":"
+
−  for DIR in $ISABELLE_DOCS
+
−  do
+
−    [ -d "$DIR" ] || fail "Bad document directory: $DIR"
+
−    [ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents"
+
−  done
+
−  IFS="$ORIG_IFS"
+
−else
+
−  ORIG_IFS="$IFS"
+
−  IFS=":"
+
−  for DIR in $ISABELLE_DOCS
+
−  do
+
−    IFS="$ORIG_IFS"
+
−    [ -d "$DIR" ] || fail "Bad document directory: $DIR"
+
−    for FMT in "$ISABELLE_DOC_FORMAT" dvi
+
−    do
+
−      [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISABELLE_TOOL" display "$DOC.$FMT"; }
+
−    done
+
−  done
+
−  IFS="$ORIG_IFS"
+
−  fail "Unknown Isabelle document: $DOC"  
+
−fi
+
−