# HG changeset patch
# User wenzelm
# Date 1001609140 -7200
# Node ID 4f26832a7b86a2ed1e49e2b23e94312fe174642a
# Parent  cd6d2eddf75f4d0fc8c7bec1ee87b92d7feb2b41
updated;

diff -r cd6d2eddf75f -r 4f26832a7b86 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Sep 27 18:45:23 2001 +0200
+++ b/src/HOL/IsaMakefile	Thu Sep 27 18:45:40 2001 +0200
@@ -155,7 +155,7 @@
 HOL-Real-ex: HOL-Real $(LOG)/HOL-Real-ex.gz
 
 $(LOG)/HOL-Real-ex.gz: $(OUT)/HOL-Real Real/ex/ROOT.ML \
-  Real/ex/BinEx.thy
+  Real/ex/BinEx.thy Real/ex/document/root.tex Real/ex/Sqrt_Irrational.thy
 	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real ex
 
 
diff -r cd6d2eddf75f -r 4f26832a7b86 src/HOL/Real/ex/ROOT.ML
--- a/src/HOL/Real/ex/ROOT.ML	Thu Sep 27 18:45:23 2001 +0200
+++ b/src/HOL/Real/ex/ROOT.ML	Thu Sep 27 18:45:40 2001 +0200
@@ -1,9 +1,9 @@
 (*  Title:      HOL/Real/ex/ROOT.ML
     ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1999  University of Cambridge
 
-HOL/Real examples.
+Miscellaneous HOL-Real Examples.
 *)
 
+no_document use_thy "Primes";
+time_use_thy "Sqrt_Irrational";
 time_use_thy "BinEx";