--- a/src/HOL/UNITY/SubstAx.ML Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Fri Oct 05 21:52:39 2001 +0200
@@ -341,9 +341,9 @@
by (auto_tac (claset() addIs prems, simpset()));
qed "LessThan_induct";
-(*Integer version. Could generalize from #0 to any lower bound*)
+(*Integer version. Could generalize from Numeral0 to any lower bound*)
val [reach, prem] =
-Goal "[| F : Always {s. (#0::int) <= f s}; \
+Goal "[| F : Always {s. (Numeral0::int) <= f s}; \
\ !! z. F : (A Int {s. f s = z}) LeadsTo \
\ ((A Int {s. f s < z}) Un B) |] \
\ ==> F : A LeadsTo B";