equal
deleted
inserted
replaced
1952 |
1952 |
1953 code_const undefined |
1953 code_const undefined |
1954 (SML "!(raise/ Fail/ \"undefined\")") |
1954 (SML "!(raise/ Fail/ \"undefined\")") |
1955 (OCaml "failwith/ \"undefined\"") |
1955 (OCaml "failwith/ \"undefined\"") |
1956 (Haskell "error/ \"undefined\"") |
1956 (Haskell "error/ \"undefined\"") |
|
1957 (Scala "!error(\"undefined\")") |
1957 |
1958 |
1958 subsubsection {* Evaluation and normalization by evaluation *} |
1959 subsubsection {* Evaluation and normalization by evaluation *} |
1959 |
1960 |
1960 setup {* |
1961 setup {* |
1961 Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of) |
1962 Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of) |