# HG changeset patch
# User wenzelm
# Date 936037768 -7200
# Node ID 66a3d3bb28e407180fe68df6b659d129f99a581a
# Parent  0fc6f18da7c5f54a6533aeb0b8f6020678c75825
clean: include HOL-Real-ex;

diff -r 0fc6f18da7c5 -r 66a3d3bb28e4 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Aug 30 17:26:43 1999 +0200
+++ b/src/HOL/IsaMakefile	Mon Aug 30 20:29:28 1999 +0200
@@ -85,6 +85,7 @@
   Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy
 	@cd Real; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Real
 
+
 ## HOL-Real-ex
 
 HOL-Real-ex: HOL-Real $(LOG)/HOL-Real-ex.gz
@@ -92,6 +93,7 @@
 $(LOG)/HOL-Real-ex.gz: $(OUT)/HOL-Real Real/ex/ROOT.ML Real/ex/BinEx.ML
 	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real ex
 
+
 ## HOL-Subst
 
 HOL-Subst: HOL $(LOG)/HOL-Subst.gz
@@ -401,4 +403,4 @@
 	  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \
 	  $(LOG)/HOL-ex.gz $(LOG)/HOL-Isar_examples.gz $(OUT)/TLA \
 	  $(LOG)/TLA.gz $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
-	  $(LOG)/TLA-Memory.gz
+	  $(LOG)/TLA-Memory.gz $(LOG)/HOL-Real-ex.gz