[isabelle] Functional Relations

In Isabelle there is a nice property, that from "f a = x" "f b = y" it 
automatically concludes that "x = y".

Sometimes I define functions as inductive relations and prove that they 
are functional, e.g. "[| (a, b) in myrel; (a, b') in myrel |] ==> b = 
b'". How to achieve that such lemmas were applied automatically?


Attachment: smime.p7s
Description: S/MIME cryptographic signature

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