Re: [isabelle] some problems with the /\ quantifier



> your recommended solution uses 'auto' which I try not to use too much because
> I'm not sure what exactly it is doing, and I prefer simple commands like
> [of ...] or 'rule_tac' for this reason. I guess this is also a kind of
> robustness consideration.

I know that others share such views, and they make sense on occasion, above all when you are trying to figure out how logic works. But itâs not a practical attitude if you want to get much work done. Assuming that you are using structured proofs, auto does not harm robustness; on the contrary, it can be more robust than single-step proofs, which often break in the presence of the slightest change. How much work will you have to do if you find yourself changing a definition?

Larry Paulson






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.