#
7f1ee5d6 |
|
14-Jan-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Provide more options for futzing with ='s precedence Now there are four functions: {temp,}_{tight,loose}_equality The temp versions create an effect that is not exported in the theory file, and can be called before new_theory without causing annoying error messages about changes being discarded. The tight precedence is 450, which is the same level as the other standard relational operators (e.g., <). The loose precedence is 100, which is historical, and clearly appropriate for = construed as iff.
|