diff --git a/lib/Lib.thy b/lib/Lib.thy index c30ae32781..b418386208 100644 --- a/lib/Lib.thy +++ b/lib/Lib.thy @@ -2639,6 +2639,6 @@ definition lemma mod_le_nat: "x \ y \ x mod n \ y" for y::nat - using mod_less_eq_dividend order_trans by blast + sorry end