# HG changeset patch
# User oheimb
# Date 962812344 -7200
# Node ID 0a85dbc4206ff42d89af226cc0b60cfe812f2484
# Parent  c71db8c2872796da54dfaf8dc1546721e6c9d89a
disambiguated := ; added Examples (factorial)

diff -r c71db8c28727 -r 0a85dbc4206f src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jul 05 17:42:06 2000 +0200
+++ b/src/HOL/IsaMakefile	Wed Jul 05 17:52:24 2000 +0200
@@ -151,7 +151,7 @@
 
 $(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Denotation.ML \
   IMP/Denotation.thy IMP/Expr.ML IMP/Expr.thy IMP/Hoare.ML IMP/Hoare.thy \
-  IMP/Natural.ML IMP/Natural.thy IMP/Example.thy IMP/ROOT.ML IMP/Transition.ML \
+  IMP/Natural.ML IMP/Natural.thy IMP/Examples.thy IMP/ROOT.ML IMP/Transition.ML\
   IMP/Transition.thy IMP/VC.ML IMP/VC.thy
 	@$(ISATOOL) usedir $(OUT)/HOL IMP