lib/Tools/doc

the splitter is now defined as a functor
moved addsplits, delsplits, Addsplits, Delsplits to Provers/splitter.ML
moved split_thm_info to Provers/splitter.ML
definined atomize via general mk_atomize
removed superfluous rot_eq_tac from simplifier.ML
HOL/simpdata.ML: renamed mk_meta_eq to meta_eq,
re-renamed mk_meta_eq_simp to mk_meta_eq
added Eps_eq to simpset

#!/bin/bash
#
# $Id$
#
# DESCRIPTION: view Isabelle documentation


PRG=$(basename $0)

function usage()
{
  echo
  echo "Usage: $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

DOCS=$(echo $ISABELLE_DOCS | tr : " ")

if [ -z "$DOC" ]; then
  for DIR in $DOCS
  do
    [ -f $DIR/Contents ] && cat $DIR/Contents
  done
else
  for DIR in $DOCS
  do
    [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi; }
  done
  fail "Unknown Isabelle document: $DOC"  
fi