Commit 20c18685 authored by Heiko Becker's avatar Heiko Becker
Browse files

add negation

parent 39e3b4ee
......@@ -304,7 +304,14 @@ val Eval_REAL_INV = Q.prove(
|> (fn th => MATCH_MP th pair_inv_v_thm)
|> add_user_proved_v_thm;
val real_neg_lem = prove (
``!(x:real). - x = 0 - x``,
fs[]);
val pair_neg_v_thm = translate real_neg_lem;
val _ = (next_ml_names := ["pair_div"])
val pair_div_v_thm = translate realTheory.real_div;
val pair_div_side_def = pair_div_v_thm
......@@ -315,6 +322,14 @@ val pair_div_v_thm =
|> DISCH_ALL |> REWRITE_RULE [pair_div_side_def] |> UNDISCH_ALL
|> add_user_proved_v_thm;
val _ = translate isSupersetInterval_def;
val divideInterval_v_thm = translate divideInterval_def;
val precond_def = fetch_thm "divideinterval_side_def"
(show_assums:=true)
val supersetInterval_v_thm = translate isSupersetInterval_def;
val validIvbounds_v_thm = translate validIntervalbounds_def;
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