equal
deleted
inserted
replaced
1732 by (thin_tac "\\<forall>M. \\<exists>x. a \\<le> x & x \\<le> b & ~ f x \\<le> M" 1); |
1732 by (thin_tac "\\<forall>M. \\<exists>x. a \\<le> x & x \\<le> b & ~ f x \\<le> M" 1); |
1733 by (dres_inst_tac [("x","1")] spec 1); |
1733 by (dres_inst_tac [("x","1")] spec 1); |
1734 by Auto_tac; |
1734 by Auto_tac; |
1735 by (res_inst_tac [("x","s")] exI 1 THEN Clarify_tac 1); |
1735 by (res_inst_tac [("x","s")] exI 1 THEN Clarify_tac 1); |
1736 by (res_inst_tac [("x","abs(f x) + 1")] exI 1 THEN Clarify_tac 1); |
1736 by (res_inst_tac [("x","abs(f x) + 1")] exI 1 THEN Clarify_tac 1); |
1737 by (dres_inst_tac [("x","xa - x")] spec 1 THEN Safe_tac); |
1737 by (dres_inst_tac [("x","xa - x")] spec 1); |
1738 by (arith_tac 1); |
1738 by (auto_tac (claset(), simpset() addsimps [abs_ge_self])); |
1739 by (arith_tac 1); |
1739 by (REPEAT (arith_tac 1)); |
1740 by (asm_full_simp_tac (simpset() addsimps [abs_ge_self]) 1); |
|
1741 by (arith_tac 1); |
|
1742 qed "isCont_bounded"; |
1740 qed "isCont_bounded"; |
1743 |
1741 |
1744 (*----------------------------------------------------------------------------*) |
1742 (*----------------------------------------------------------------------------*) |
1745 (* Refine the above to existence of least upper bound *) |
1743 (* Refine the above to existence of least upper bound *) |
1746 (*----------------------------------------------------------------------------*) |
1744 (*----------------------------------------------------------------------------*) |