Added `arbitrary'

--- a/src/HOL/HOL.thy	Fri May 23 14:52:45 1997 +0200
+++ b/src/HOL/HOL.thy	Fri May 23 18:17:53 1997 +0200
@@ -176,6 +176,9 @@
   o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
   if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
 
+constdefs arbitrary :: 'a
+         "arbitrary == @x.False"
+
 end
 
 

--- a/src/HOL/Induct/SList.thy	Fri May 23 14:52:45 1997 +0200
+++ b/src/HOL/Induct/SList.thy	Fri May 23 18:17:53 1997 +0200
@@ -100,8 +100,8 @@
   Abs_map_def "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)"
 
   null_def      "null(xs)            == list_rec xs True (%x xs r.False)"
-  hd_def        "hd(xs)              == list_rec xs (@x.True) (%x xs r.x)"
-  tl_def        "tl(xs)              == list_rec xs (@xs.True) (%x xs r.xs)"
+  hd_def        "hd(xs)              == list_rec xs arbitrary (%x xs r.x)"
+  tl_def        "tl(xs)              == list_rec xs arbitrary (%x xs r.xs)"
   (* a total version of tl: *)
   ttl_def       "ttl(xs)             == list_rec xs [] (%x xs r.xs)"
 

--- a/src/HOL/List.thy	Fri May 23 14:52:45 1997 +0200
+++ b/src/HOL/List.thy	Fri May 23 18:17:53 1997 +0200
@@ -49,10 +49,10 @@
   pred_list_def "pred_list == {(x,y). ? h. y = h#x}"
 
 primrec hd list
-  "hd([]) = (@x.False)"
+  "hd([]) = arbitrary"
   "hd(x#xs) = x"
 primrec tl list
-  "tl([]) = (@x.False)"
+  "tl([]) = arbitrary"
   "tl(x#xs) = xs"
 primrec ttl list
   (* a "total" version of tl: *)

--- a/src/HOL/WF.ML	Fri May 23 14:52:45 1997 +0200
+++ b/src/HOL/WF.ML	Fri May 23 18:17:53 1997 +0200
@@ -102,7 +102,7 @@
 (*** is_recfun ***)
 
 goalw WF.thy [is_recfun_def,cut_def]
-    "!!f. [| is_recfun r H a f;  ~(b,a):r |] ==> f(b) = (@z.True)";
+    "!!f. [| is_recfun r H a f;  ~(b,a):r |] ==> f(b) = arbitrary";
 by (etac ssubst 1);
 by (asm_simp_tac HOL_ss 1);
 qed "is_recfun_undef";

--- a/src/HOL/WF.thy	Fri May 23 14:52:45 1997 +0200
+++ b/src/HOL/WF.thy	Fri May 23 18:17:53 1997 +0200
@@ -13,7 +13,7 @@
   "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
 
   cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
-  "cut f r x == (%y. if (y,x):r then f y else @z.True)"
+  "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
 
   is_recfun  :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
   "is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"