I want to prove ``a <> b`` for some a,b. After stripping I am asked to prove F. I was able to use the assumptions to prove ``F = T``. At this point I thought "asm_simp_tac bool_ss []" should finish the proof but it doesn't. So "pop_assum (fn th => rewrite_tac [th]" actually finished the work for me. Is this to be expected?
Thanks, Haitao
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
