# HG changeset patch
# User lcp
# Date 798800209 -7200
# Node ID 66efd8f90fbdd45586dc8c3f767b76712e97a707
# Parent  e0f2dffab5067d3fc87819e2c50e575821d0c76a
Now loads the theory "Let".  Could add it to FOL, but this appears to
be incompatible with CCL.

diff -r e0f2dffab506 -r 66efd8f90fbd src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Sat Apr 22 13:25:31 1995 +0200
+++ b/src/ZF/ROOT.ML	Tue Apr 25 10:56:49 1995 +0200
@@ -32,6 +32,7 @@
 use     "../Pure/section_utils.ML";
 use     "thy_syntax.ML";
 
+use_thy "Let";
 use_thy "InfDatatype";
 use_thy "List";
 use_thy "EquivClass";