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
     1 (*  Title:      HOL/Quot/ROOT.ML
     2     ID:         $Id$
     3     Author:     
     4     Copyright   
     5 
     6 Higher-order quotients.
     7 *)
     8 
     9 writeln"Root file for HOL/Quot";
    10 
    11 use_thy "FRACT";