# HG changeset patch
# User haftmann
# Date 1138721178 -3600
# Node ID f8e4322c9567bcb1760d01a5acebd10c82a7ba34
# Parent  378c0cb028a83cdda1bae953a088ef66bf561c13
added serialization for arbitrary

diff -r 378c0cb028a8 -r f8e4322c9567 src/HOL/HOL.thy
--- 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