author | paulson |
Thu, 03 Apr 1997 10:30:23 +0200 | |
changeset 2882 | 2563063772d9 |
parent 2881 | 62ecde1015ae |
child 2883 | fd1c0b8e9b61 |
--- 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;