# HG changeset patch
# User wenzelm
# Date 1085166892 -7200
# Node ID c0401da7726da5b7e7e1643e006bacdb2d19a440
# Parent  bafb24c150c17cef022b4dc59341512e6422ff05
use plain SOME;

diff -r bafb24c150c1 -r c0401da7726d src/HOL/Bali/State.thy
--- a/src/HOL/Bali/State.thy	Fri May 21 21:14:18 2004 +0200
+++ b/src/HOL/Bali/State.thy	Fri May 21 21:14:52 2004 +0200
@@ -41,7 +41,7 @@
 constdefs
   
   the_Arr :: "obj option \<Rightarrow> ty \<times> int \<times> (vn, val) table"
- "the_Arr obj \<equiv> \<epsilon>(T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>"
+ "the_Arr obj \<equiv> SOME (T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>"
 
 lemma the_Arr_Arr [simp]: "the_Arr (Some \<lparr>tag=Arr T k,values=cs\<rparr>) = (T,k,cs)"
 apply (auto simp: the_Arr_def)
@@ -266,7 +266,7 @@
 
 constdefs
   new_Addr     :: "heap \<Rightarrow> loc option"
- "new_Addr h   \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (\<epsilon> a. h a = None)"
+ "new_Addr h   \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (SOME a. h a = None)"
 
 lemma new_AddrD: "new_Addr h = Some a \<Longrightarrow> h a = None"
 apply (unfold new_Addr_def)
diff -r bafb24c150c1 -r c0401da7726d src/HOL/Bali/Type.thy
--- a/src/HOL/Bali/Type.thy	Fri May 21 21:14:18 2004 +0200
+++ b/src/HOL/Bali/Type.thy	Fri May 21 21:14:52 2004 +0200
@@ -51,7 +51,7 @@
 
 constdefs
   the_Class :: "ty \<Rightarrow> qtname"
- "the_Class T \<equiv> \<epsilon> C. T = Class C" (** primrec not possible here **)
+ "the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **)
  
 lemma the_Class_eq [simp]: "the_Class (Class C)= C"
 by (auto simp add: the_Class_def)
diff -r bafb24c150c1 -r c0401da7726d src/HOL/Infinite_Set.thy
--- a/src/HOL/Infinite_Set.thy	Fri May 21 21:14:18 2004 +0200
+++ b/src/HOL/Infinite_Set.thy	Fri May 21 21:14:52 2004 +0200
@@ -245,8 +245,8 @@
   assumes inf: "infinite (S::'a set)"
   shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
 proof -
-  def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {\<epsilon> e. e \<in> T})"
-  def pick \<equiv> "\<lambda>n. (\<epsilon> e. e \<in> Sseq n)"
+  def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
+  def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
   have Sseq_inf: "\<And>n. infinite (Sseq n)"
   proof -
     fix n