# HG changeset patch
# User nipkow
# Date 864404273 -7200
# Node ID 3a5e4930fb77d5c1ca17ee76ddb6bd56ed6365a3
# Parent  0206e7507737d25e454a7e3289c6cb2e448483ee
Added `arbitrary'

diff -r 0206e7507737 -r 3a5e4930fb77 src/HOL/HOL.thy
--- 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
 
 
diff -r 0206e7507737 -r 3a5e4930fb77 src/HOL/Induct/SList.thy
--- 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)"
 
diff -r 0206e7507737 -r 3a5e4930fb77 src/HOL/List.thy
--- 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: *)
diff -r 0206e7507737 -r 3a5e4930fb77 src/HOL/WF.ML
--- 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";
diff -r 0206e7507737 -r 3a5e4930fb77 src/HOL/WF.thy
--- 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)"