# HG changeset patch
# User wenzelm
# Date 1005086734 -3600
# Node ID 10941435e5f4a9c2532e7019ede4f5b1d2adb532
# Parent  b4401452928eed371882e20b46c7237bc168e123
renamed Real/ex/Sqrt_Irrational.thy to Real/ex/Sqrt.thy;
added ex/Locales.thy;

diff -r b4401452928e -r 10941435e5f4 src/HOL/IsaMakefile
--- 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 \