src/HOL/UNITY/SubstAx.ML

 by (Asm_simp_tac 1);
 qed "LessThan_induct";
 
 (*Integer version.  Could generalize from #0 to any lower bound*)
 val [reach, prem] =
-Goal "[| F : Always {s. #0 <= f s};  \
+Goal "[| F : Always {s. (#0::int) <= f s};  \
 \        !! z. F : (A Int {s. f s = z}) LeadsTo                     \
 \                           ((A Int {s. f s < z}) Un B) |] \
 \     ==> F : A LeadsTo B";
 by (res_inst_tac [("f", "nat o f")] (allI RS LessThan_induct) 1);
 by (simp_tac (simpset() addsimps [vimage_def]) 1);