src/HOL/Quot/ROOT.ML
author wenzelm
Sun, 30 Jul 2000 12:48:55 +0200
changeset 9460 53d7ad5bec39
parent 9000 c20d58286a51
permissions -rw-r--r--
Logic.goal_const;

(*  Title:      HOL/Quot/ROOT.ML
    ID:         $Id$

Higher-order quotients.
*)

time_use_thy "FRACT";