# HG changeset patch
# User wenzelm
# Date 1015433762 -3600
# Node ID d7bb6e4f5f8281448690ef4928d59c6b6aaba590
# Parent  d6a09050a40d2da9310de822252855a0f5696258
tuned;

diff -r d6a09050a40d -r d7bb6e4f5f82 src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Wed Mar 06 17:55:10 2002 +0100
+++ b/src/FOL/cladata.ML	Wed Mar 06 17:56:02 2002 +0100
@@ -12,7 +12,7 @@
 structure Make_Elim = Make_Elim_Fun(val classical = classical);
 
 (*we don't redeclare the original make_elim (Tactic.make_elim) for 
-  compatibliity with strange things done in many existing proofs *)
+  compatibility with strange things done in many existing proofs *)
 val cla_make_elim = Make_Elim.make_elim;
 
 (*** Applying ClassicalFun to create a classical prover ***)
diff -r d6a09050a40d -r d7bb6e4f5f82 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Mar 06 17:55:10 2002 +0100
+++ b/src/HOL/IsaMakefile	Wed Mar 06 17:56:02 2002 +0100
@@ -182,9 +182,9 @@
 
 HOL-Hyperreal-ex: HOL-Hyperreal $(LOG)/HOL-Hyperreal-ex.gz
 
-$(LOG)/HOL-Hyperreal-ex.gz: $(OUT)/HOL-Hyperreal Hyperreal/ex/ROOT.ML \
-  Hyperreal/ex/document/root.tex Hyperreal/ex/Sqrt.thy \
-  Hyperreal/ex/Sqrt_Script.thy
+$(LOG)/HOL-Hyperreal-ex.gz: $(OUT)/HOL-Hyperreal Library/Primes.thy \
+  Hyperreal/ex/ROOT.ML Hyperreal/ex/document/root.tex \
+  Hyperreal/ex/Sqrt.thy Hyperreal/ex/Sqrt_Script.thy
 	@cd Hyperreal; $(ISATOOL) usedir $(OUT)/HOL-Hyperreal ex