Declares overloading for if-and-only-if
authorpaulson
Thu, 03 Apr 1997 10:30:23 +0200
changeset 2882 2563063772d9
parent 2881 62ecde1015ae
child 2883 fd1c0b8e9b61
Declares overloading for if-and-only-if
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;