equal
deleted
inserted
replaced
316 |
316 |
317 instance .. |
317 instance .. |
318 |
318 |
319 end |
319 end |
320 |
320 |
321 definition (in term_syntax) [code_unfold]: |
321 context |
|
322 includes term_syntax |
|
323 begin |
|
324 |
|
325 definition [code_unfold]: |
322 "valtermify_float x y = Code_Evaluation.valtermify Float {\<cdot>} x {\<cdot>} y" |
326 "valtermify_float x y = Code_Evaluation.valtermify Float {\<cdot>} x {\<cdot>} y" |
|
327 |
|
328 end |
323 |
329 |
324 instantiation float :: full_exhaustive |
330 instantiation float :: full_exhaustive |
325 begin |
331 begin |
326 |
332 |
327 definition |
333 definition |