src/Pure/Interface/ROOT.ML
author paulson
Thu, 25 May 2000 15:12:40 +0200
changeset 8970 3ac901561f33
parent 6697 40f2fe61b47e
child 11909 92e442b783db
permissions -rw-r--r--
deleted sum_below: no need for it with setsum and lessThan

(*  Title:      Pure/Interface/ROOT.ML
    ID:         $Id$

Miscellaneous interfaces.
*)

use "proof_general.ML";
use "isamode.ML";