--- 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 ***)
--- 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