Declares overloading for if-and-only-if
authorpaulson
Thu Apr 03 10:30:23 1997 +0200 (1997-04-03)
changeset 28822563063772d9
parent 2881 62ecde1015ae
child 2883 fd1c0b8e9b61
Declares overloading for if-and-only-if
src/HOL/cladata.ML
     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;