# HG changeset patch # User wenzelm # Date 860154971 -7200 # Node ID d7bff1252d1ea45f4df96554653b651d424fcb5a # Parent 27dc4862751b2164f76083ce1b65c659e42d1cd7 Higher-order quotients. diff -r 27dc4862751b -r d7bff1252d1e src/HOL/Quot/README diff -r 27dc4862751b -r d7bff1252d1e src/HOL/Quot/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quot/ROOT.ML Fri Apr 04 13:56:11 1997 +0200 @@ -0,0 +1,13 @@ +(* Title: HOL/Quot/ROOT.ML + ID: $Id$ + Author: + Copyright + +Higher-order quotients. +*) + +HOL_build_completed; (*Make examples fail if HOL did*) + +writeln"Root file for HOL/Quot"; + +use_thy "Quot";