src/HOL/Quot/ROOT.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 6349 f7750d816c21
child 9000 c20d58286a51
permissions -rw-r--r--
tidied; added lemma restrict_to_left
wenzelm@2898
     1
(*  Title:      HOL/Quot/ROOT.ML
wenzelm@2898
     2
    ID:         $Id$
wenzelm@2898
     3
    Author:     
wenzelm@2898
     4
    Copyright   
wenzelm@2898
     5
wenzelm@2898
     6
Higher-order quotients.
wenzelm@2898
     7
*)
wenzelm@2898
     8
wenzelm@2898
     9
writeln"Root file for HOL/Quot";
wenzelm@2898
    10
slotosch@2908
    11
use_thy "FRACT";