# 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