src/HOL/cladata.ML
changeset 2882 2563063772d9
parent 2860 6dde30a9e905
child 3004 8036aaf49f70
equal deleted inserted replaced
2881:62ecde1015ae 2882:2563063772d9
    74   val claset	= Classical.claset
    74   val claset	= Classical.claset
    75   val rep_claset = Classical.rep_claset
    75   val rep_claset = Classical.rep_claset
    76   end;
    76   end;
    77 
    77 
    78 structure Blast = BlastFun(Blast_Data);
    78 structure Blast = BlastFun(Blast_Data);
       
    79 Blast.declConsts (["op ="], [iffI]);	(*overloading of equality as iff*)
    79 
    80 
    80 val Blast_tac = Blast.Blast_tac
    81 val Blast_tac = Blast.Blast_tac
    81 and blast_tac = Blast.blast_tac;
    82 and blast_tac = Blast.blast_tac;