changeset 18867 | f8e4322c9567 |
parent 18832 | 6ab4de872a70 |
child 18887 | 6ad81e3fa478 |
--- a/src/HOL/HOL.thy Tue Jan 31 16:15:51 2006 +0100 +++ b/src/HOL/HOL.thy Tue Jan 31 16:26:18 2006 +0100 @@ -1376,6 +1376,7 @@ "op *" "IntDef.op_times" Not "HOL.not" uminus "HOL.uminus" + arbitrary "HOL.arbitrary" code_syntax_tyco bool ml (target_atom "bool") @@ -1397,5 +1398,8 @@ "op =" (* an intermediate solution *) ml (infixl 6 "=") haskell (infixl 4 "==") + arbitrary + ml ("raise/ (Fail/ \"non-defined-result\")") + haskell ("error/ \"non-defined result\"") end