Commit a2c542f0 authored by Heiko Becker's avatar Heiko Becker
Browse files

Merge branch 'hol4' of gitlab.mpi-sws.org:hbecker/daisy into hol4

parents a276c266 05bda039
......@@ -49,18 +49,12 @@ val err_up = store_thm ("err_up",
a - b <= c /\
0 < a - b ==>
b <= a + c``,
rpt (strip_tac) \\
`b < a` by REAL_ASM_ARITH_TAC \\
`a <= b + c` by REAL_ASM_ARITH_TAC \\
`b + c <= a + c` by REAL_ASM_ARITH_TAC \\
REAL_ASM_ARITH_TAC);
val REAL_LE_ADD_FLIP = store_thm ("REAL_LE_ADD_FLIP",
``!a b (c:real).
a - b <= c ==>
a - c <= b``,
rpt (strip_tac) \\
`a - b - c <= 0` by REAL_ASM_ARITH_TAC \\
REAL_ASM_ARITH_TAC);
val _ = export_theory();
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment