equal
deleted
inserted
replaced
1659 ("x","abs(y - f x)")] spec 1); |
1659 ("x","abs(y - f x)")] spec 1); |
1660 by Safe_tac; |
1660 by Safe_tac; |
1661 by (asm_full_simp_tac (simpset() addsimps []) 1); |
1661 by (asm_full_simp_tac (simpset() addsimps []) 1); |
1662 by (dres_inst_tac [("x","s")] spec 1); |
1662 by (dres_inst_tac [("x","s")] spec 1); |
1663 by (Clarify_tac 1); |
1663 by (Clarify_tac 1); |
1664 by (cut_inst_tac [("R1.0","f x"),("R2.0","y")] real_linear 1); |
1664 by (cut_inst_tac [("x","f x"),("y","y")] linorder_less_linear 1); |
1665 by Safe_tac; |
1665 by Safe_tac; |
1666 by (dres_inst_tac [("x","ba - x")] spec 1); |
1666 by (dres_inst_tac [("x","ba - x")] spec 1); |
1667 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [abs_iff]))); |
1667 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [abs_iff]))); |
1668 by (dres_inst_tac [("x","aa - x")] spec 1); |
1668 by (dres_inst_tac [("x","aa - x")] spec 1); |
1669 by (case_tac "x \\<le> aa" 1); |
1669 by (case_tac "x \\<le> aa" 1); |