Re: [isabelle-dev] Default simprules for division in fields

2014-04-06 Thread Thomas Sewell
This makes me realise that I may have been misunderstanding field_simps. I've been using it as a replacement after ring_simps disappeared a while ago. It always struck me as odd, since I'm nearly always in a word type, which is a ring but not a field. Is it just a coincidence that field_simps

Re: [isabelle-dev] Default simprules for division in fields

2014-04-06 Thread Tobias Nipkow
You can use algebra_simps for everything up to and including rings. Field_simps is separate because it can rearrange your formula dramatically by multiplying with all the denominators - you don't always want that. Tobias On 07/04/2014 03:11, Thomas Sewell wrote: This makes me realise that I may