src/HOL/UNITY/WFair.ML
changeset 8948 b797cfa3548d
parent 8835 56187238220d
child 9084 090d450af656
--- a/src/HOL/UNITY/WFair.ML	Wed May 24 18:19:04 2000 +0200
+++ b/src/HOL/UNITY/WFair.ML	Wed May 24 18:40:01 2000 +0200
@@ -400,14 +400,14 @@
 
 (*Alternative proof is via the lemma F : (A Int f-``(lessThan m)) leadsTo B*)
 val prems = 
-Goal "[| !!m. F : (A Int f-``{m}) leadsTo ((A Int f-``(lessThan m)) Un B) |] \
+Goal "[| !!m::nat. F : (A Int f-``{m}) leadsTo ((A Int f-``{..m(}) Un B) |] \
 \     ==> F : A leadsTo B";
 by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
 by (Asm_simp_tac 1);
 by (blast_tac (claset() addIs prems) 1);
 qed "lessThan_induct";
 
-Goal "[| ALL m:(greaterThan l).    \
+Goal "!!l::nat. [| ALL m:(greaterThan l).    \
 \           F : (A Int f-``{m}) leadsTo ((A Int f-``(lessThan m)) Un B) |] \
 \     ==> F : A leadsTo ((A Int (f-``(atMost l))) Un B)";
 by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, 
@@ -416,7 +416,7 @@
 by (Asm_simp_tac 1);
 qed "lessThan_bounded_induct";
 
-Goal "[| ALL m:(lessThan l).    \
+Goal "!!l::nat. [| ALL m:(lessThan l).    \
 \           F : (A Int f-``{m}) leadsTo ((A Int f-``(greaterThan m)) Un B) |] \
 \     ==> F : A leadsTo ((A Int (f-``(atLeast l))) Un B)";
 by (res_inst_tac [("f","f"),("f1", "%k. l - k")]