diff --git a/Makefile b/Makefile
deleted file mode 100644
index ad88157..0000000
--- a/Makefile
+++ /dev/null
@@ -1,83 +0,0 @@
-############################################################################
-#
-#  Primary targets:
-#    all           - the default target; synonym for 'coq'
-#    coq           - builds all .vo files
-#    doc           - synonym for 'documentation'
-#    install       - copy to coq library location
-#    clean         - removes generated files
-#
-#  Other targets (intended to be used by the developers of this library):
-#    gens          - builds generated .v files on demand
-#    dist          - builds a zip file for distribution
-#
-############################################################################
-
-## Paths to executables. Do not include options here.
-## Modify these to suit your Coq installation, if necessary.
-
-## If you get warnings such as:
-## *** Warning: in file AssocList.v, library CoqFSetDecide is required and has not been found in the loadpath!
-## you can use a shell variable to set the load path. (Somehow the -I below is being ignored.)
-## export COQPATH=.
-
-COQC = coqc
-COQDEP = coqdep
-COQDOC = coqdoc
-
-
-## Library name used for the imports in Coq
-
-LIBNAME=Metalib
-
-## Name of the submakefile generated by coq_makefile
-
-COQMKFILENAME=CoqSrc.mk
-
-
-############################################################################
-
-.PHONY: all clean coq dist doc gens
-.SUFFIXES: .v .vo .v.d .v.glob
-
-all: coq
-
-$(COQMKFILENAME): Makefile
-	{ echo "-R $(LIBNAME) $(LIBNAME) " ; ls $(LIBNAME)/*.v ; } > _CoqProject && coq_makefile -f _CoqProject -o $(COQMKFILENAME)
-
-coq: $(COQMKFILENAME)
-	@$(MAKE) -f $(COQMKFILENAME)
-
-doc:
-	@$(MAKE) -f $(COQMKFILENAME) html
-
-install:
-	@$(MAKE) -f $(COQMKFILENAME) install
-
-clean:
-	@$(MAKE) -f $(COQMKFILENAME) clean
-
-
-############################################################################
-
-DATE = $(shell date +%Y%m%d)
-DIR  = metalib-$(DATE)
-
-COQSPLIT = ../../books/sf/tools/coqsplit
-STLC = ../../books/coqbook/stlc/STLC.v
-
-gens:
-	make -C ../../books/sf tools/coqsplit
-	$(COQSPLIT) < $(STLC) > STLC.v
-	$(COQSPLIT) -solutions < $(STLC) > STLCsol.v
-
-dist:
-	svn export . $(DIR)
-	(cd $(DIR); $(MAKE) documentation)
-	rm -f $(DIR)/*.vo $(DIR)/*.glob
-	rm -f $(DIR)/TODO.txt
-	echo Release $(DATE) / svn revision `svnversion .` >> $(DIR)/VERSION
-	zip -r $(DIR).zip $(DIR)
-	@echo
-	@echo Done.
-	@echo See $(DIR) and $(DIR).zip.
diff --git a/README.md b/README.md
index d7d8d69..517bf4d 100644
--- a/README.md
+++ b/README.md
@@ -3,9 +3,9 @@ COMPILATION, INSTALLATION, AND DOCUMENTATION:
   This library requires Coq 8.6, available via [opam](https://opam.ocaml.org/)
   or from the Coq website [https://coq.inria.fr/download].
 
-  To compile the library:
+  To compile the library, in the [Metalib](Metalib/) directory:
 
-     `make`          generate Coq makefile, compile Coq files
+     `make`           generate Coq makefile, compile Coq files
 	  `make html`     generate Coq documentation
 	  `make install`  install library on your system
 
@@ -16,9 +16,12 @@ TUTORIAL:
 
   The metatheory library comes with a short tutorial.  The main files for the
   tutorial are STLC.v, and STLCsol.v.  Make sure that you've compiled the
-  library first. The file [STLC.v](STLC.v) contains an introduction to
+  library first. The file [STLC.v](Tutorial/STLC.v) contains an introduction to
   mechanizing programming language definitions with binding in Coq and how to
-  reason about them.  Solutions to exercises are in [STLCsol.v](STLCsol.v).
+  reason about them.  Solutions to exercises are in [STLCsol.v](Tutorial/STLCsol.v).
+
+  An additional example of the library is available in the
+  [Fsub](Fsub/) directory.
 
   Those new to Coq should start with Software Foundations, which is an
   introduction to using Coq. The tutorial assumes some familarity with