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.
renamed Real/ex/Sqrt_Irrational.thy to Real/ex/Sqrt.thy;
authorwenzelm
Tue, 06 Nov 2001 23:45:34 +0100
changeset 12074 10941435e5f4
parent 12073 b4401452928e
child 12075 8d65dd96381f
renamed Real/ex/Sqrt_Irrational.thy to Real/ex/Sqrt.thy; added ex/Locales.thy;
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions 
--- a/src/HOL/IsaMakefile	Tue Nov 06 19:29:36 2001 +0100
+++ b/src/HOL/IsaMakefile	Tue Nov 06 23:45:34 2001 +0100
@@ -154,8 +154,8 @@
 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/document/root.tex Real/ex/Sqrt_Irrational.thy\
-      Real/ex/Sqrt_Script.thy
+  Real/ex/BinEx.thy Real/ex/document/root.tex Real/ex/Sqrt.thy \
+  Real/ex/Sqrt_Script.thy
 	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real ex
 
 
@@ -525,7 +525,7 @@
 $(LOG)/HOL-ex.gz: $(OUT)/HOL ex/AVL.ML ex/AVL.thy ex/Antiquote.thy \
   ex/BT.thy ex/BinEx.thy ex/Group.ML ex/Group.thy \
   ex/Hilbert_Classical.thy ex/InSort.ML ex/InSort.thy ex/IntRing.ML \
-  ex/IntRing.thy ex/Lagrange.ML ex/Lagrange.thy \
+  ex/IntRing.thy ex/Lagrange.ML ex/Lagrange.thy ex/Locales.thy \
   ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy \
   ex/NatSum.thy ex/PER.thy ex/Primrec.thy ex/Puzzle.ML ex/Puzzle.thy \
   ex/Qsort.ML ex/Qsort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
isabelle