equal
deleted
inserted
replaced
707 evaluation in Standard ML. The following attempt would make @{ML |
707 evaluation in Standard ML. The following attempt would make @{ML |
708 REPEAT}~@{text "tac"} loop: |
708 REPEAT}~@{text "tac"} loop: |
709 \end{warn} |
709 \end{warn} |
710 \<close> |
710 \<close> |
711 |
711 |
712 ML \<open> |
712 ML_val \<open> |
713 (*BAD -- does not terminate!*) |
713 (*BAD -- does not terminate!*) |
714 fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac; |
714 fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac; |
715 \<close> |
715 \<close> |
716 |
716 |
717 |
717 |