Commit 7ab5c59a authored by Heiko Becker's avatar Heiko Becker
Browse files

Remove unused search term

parent 0c434c2b
......@@ -22,5 +22,3 @@ let REAL_ABS_ERR_SIMPL =
intros "!a b"
THEN REWRITE_TAC [REAL_ADD_LDISTRIB; REAL_MUL_RID; REAL_ADD_SUB2; REAL_ABS_NEG]
THEN auto);;
search [`abs (-- (a:real))`];;
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