1.1 --- a/src/HOL/UNITY/SubstAx.ML	Mon Oct 22 11:01:30 2001 +0200
     1.2 +++ b/src/HOL/UNITY/SubstAx.ML	Mon Oct 22 11:54:22 2001 +0200
     1.3 @@ -341,9 +341,9 @@
     1.4  by (auto_tac (claset() addIs prems, simpset()));
     1.5  qed "LessThan_induct";
     1.6  
     1.7 -(*Integer version.  Could generalize from Numeral0 to any lower bound*)
     1.8 +(*Integer version.  Could generalize from 0 to any lower bound*)
     1.9  val [reach, prem] =
    1.10 -Goal "[| F : Always {s. (Numeral0::int) <= f s};  \
    1.11 +Goal "[| F : Always {s. (0::int) <= f s};  \
    1.12  \        !! z. F : (A Int {s. f s = z}) LeadsTo                     \
    1.13  \                           ((A Int {s. f s < z}) Un B) |] \
    1.14  \     ==> F : A LeadsTo B";