# HG changeset patch # User paulson # Date 860056223 -7200 # Node ID 2563063772d9bc2ad6e5f02b24f9c533104b0590 # Parent 62ecde1015ae8a7688dcbdb243c23992be1bdc4b Declares overloading for if-and-only-if diff -r 62ecde1015ae -r 2563063772d9 src/HOL/cladata.ML --- a/src/HOL/cladata.ML Thu Apr 03 10:29:57 1997 +0200 +++ b/src/HOL/cladata.ML Thu Apr 03 10:30:23 1997 +0200 @@ -76,6 +76,7 @@ end; structure Blast = BlastFun(Blast_Data); +Blast.declConsts (["op ="], [iffI]); (*overloading of equality as iff*) val Blast_tac = Blast.Blast_tac and blast_tac = Blast.blast_tac;