--- a/src/HOL/Complex/ex/MIR.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Complex/ex/MIR.thy Sun Oct 21 14:53:44 2007 +0200
@@ -268,7 +268,7 @@
| "fmsize (NDvd i t) = 2"
| "fmsize p = 1"
(* several lemmas about fmsize *)
-lemma fmsize_pos: "fmsize p > 0"
+lemma fmsize_pos: "fmsize p \<noteq> 0"
by (induct p rule: fmsize.induct) simp_all
(* Semantics of formulae (fm) *)
@@ -316,7 +316,7 @@
"prep (Imp p q) = prep (Or (NOT p) q)"
"prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
"prep p = p"
-(hints simp add: fmsize_pos)
+(hints simp add: fmsize_pos neq0_conv[symmetric])
lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
by (induct p rule: prep.induct, auto)