448 \item real numbers, \hyperpage{136--137} |
448 \item real numbers, \hyperpage{136--137} |
449 \item \isacommand {recdef} (command), \hyperpage{45--50}, |
449 \item \isacommand {recdef} (command), \hyperpage{45--50}, |
450 \hyperpage{98}, \hyperpage{160--168} |
450 \hyperpage{98}, \hyperpage{160--168} |
451 \subitem and numeric literals, \hyperpage{132} |
451 \subitem and numeric literals, \hyperpage{132} |
452 \item \isa {recdef_cong} (attribute), \hyperpage{164} |
452 \item \isa {recdef_cong} (attribute), \hyperpage{164} |
453 \item \isa {recdef_simp}, \bold{47} |
453 \item \isa {recdef_simp} (attribute), \hyperpage{47} |
454 \item \isa {recdef_wf}, \bold{162} |
454 \item \isa {recdef_wf} (attribute), \hyperpage{162} |
455 \item \isacommand {record} (command), \hyperpage{140} |
455 \item \isacommand {record} (command), \hyperpage{140} |
456 \item \isa {record_split} (method), \hyperpage{143} |
456 \item \isa {record_split} (method), \hyperpage{143} |
457 \item records, \hyperpage{140--144} |
457 \item records, \hyperpage{140--144} |
458 \subitem extensible, \hyperpage{141--142} |
458 \subitem extensible, \hyperpage{141--142} |
459 \item recursion |
459 \item recursion |