Re: [isabelle] trying to convince Isabelle to accept some programming



So my question is: do I need to write my own rewrite engine/tactical, or would a proper use of existing ones in Isabelle solve my problems regarding the possibility of decomposition and its computational complexity ?

I cannot predict that, but your exclusive use of tactic "auto" is probably the source of your problems. As you say, it tries too hard. In which case you should not use it but use "simp" instead, which is more predictable.

Tobias





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