# HG changeset patch
# User nipkow
# Date 830623902 -7200
# Node ID 0bcc8cab3461d5bdc8a5c263538c96f26b0a11d8
# Parent  bf46e4acc6821127cd7d94d5fc5275601d326e57
Forgot to add Expr to IMP.

diff -r bf46e4acc682 -r 0bcc8cab3461 src/HOL/Makefile
--- a/src/HOL/Makefile	Sat Apr 27 18:50:39 1996 +0200
+++ b/src/HOL/Makefile	Sat Apr 27 18:51:42 1996 +0200
@@ -74,7 +74,7 @@
 	esac
 
 ##IMP-semantics example
-IMP_NAMES = Com Natural Transition Denotation Hoare VC
+IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
 
 IMP:    $(BIN)/HOL  $(IMP_FILES)