Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
updated;
authorwenzelm
Thu, 27 Sep 2001 18:45:40 +0200
changeset 11598 4f26832a7b86
parent 11597 cd6d2eddf75f
child 11599 12cc28aafb4d
updated;
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions
src/HOL/Real/ex/ROOT.ML file | annotate | diff | comparison | revisions 
--- 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
 
 
--- 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";
isabelle