equal
deleted
inserted
replaced
408 |
408 |
409 local structure P = OuterParse and K = OuterKeyword in |
409 local structure P = OuterParse and K = OuterKeyword in |
410 |
410 |
411 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; |
411 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; |
412 |
412 |
413 val nbeP = |
413 val _ = |
414 OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag |
414 OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag |
415 (opt_modes -- P.typ >> (Toplevel.keep o norm_print_term_cmd)); |
415 (opt_modes -- P.typ >> (Toplevel.keep o norm_print_term_cmd)); |
416 |
416 |
417 val _ = OuterSyntax.add_parsers [nbeP]; |
|
418 |
|
419 end; |
417 end; |
420 |
418 |
421 end; |
419 end; |