:: deftheorem defines N_Real CAYLDICK:def 8 :
N_Real = ConjNormAlgStr(# REAL,multreal,addreal,multreal,(In (1,REAL)),(In (0,REAL)),absreal,(id REAL) #);