src/HOL/cladata.ML
changeset 2882 2563063772d9
parent 2860 6dde30a9e905
child 3004 8036aaf49f70
     1.1 --- a/src/HOL/cladata.ML	Thu Apr 03 10:29:57 1997 +0200
     1.2 +++ b/src/HOL/cladata.ML	Thu Apr 03 10:30:23 1997 +0200
     1.3 @@ -76,6 +76,7 @@
     1.4    end;
     1.5  
     1.6  structure Blast = BlastFun(Blast_Data);
     1.7 +Blast.declConsts (["op ="], [iffI]);	(*overloading of equality as iff*)
     1.8  
     1.9  val Blast_tac = Blast.Blast_tac
    1.10  and blast_tac = Blast.blast_tac;