Commit 3b4f3771 authored by Heiko Becker's avatar Heiko Becker

Fix compilation

parent c20bfa60
......@@ -362,7 +362,4 @@ qpat_x_assum `!x. (A /\ B) \/ C` (fn thm => qspecl_then [`nR - nF` ] DISJ_CASES_
**)
**)
DB.match [] ``a * (b:real) <= c * d``
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