use plain SOME;
authorwenzelm
Fri May 21 21:14:52 2004 +0200 (2004-05-21)
changeset 14766c0401da7726d
parent 14765 bafb24c150c1
child 14767 d2b071e65e4c
use plain SOME;
src/HOL/Bali/State.thy
src/HOL/Bali/Type.thy
src/HOL/Infinite_Set.thy
     1.1 --- a/src/HOL/Bali/State.thy	Fri May 21 21:14:18 2004 +0200
     1.2 +++ b/src/HOL/Bali/State.thy	Fri May 21 21:14:52 2004 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4  constdefs
     1.5    
     1.6    the_Arr :: "obj option \<Rightarrow> ty \<times> int \<times> (vn, val) table"
     1.7 - "the_Arr obj \<equiv> \<epsilon>(T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>"
     1.8 + "the_Arr obj \<equiv> SOME (T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>"
     1.9  
    1.10  lemma the_Arr_Arr [simp]: "the_Arr (Some \<lparr>tag=Arr T k,values=cs\<rparr>) = (T,k,cs)"
    1.11  apply (auto simp: the_Arr_def)
    1.12 @@ -266,7 +266,7 @@
    1.13  
    1.14  constdefs
    1.15    new_Addr     :: "heap \<Rightarrow> loc option"
    1.16 - "new_Addr h   \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (\<epsilon> a. h a = None)"
    1.17 + "new_Addr h   \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (SOME a. h a = None)"
    1.18  
    1.19  lemma new_AddrD: "new_Addr h = Some a \<Longrightarrow> h a = None"
    1.20  apply (unfold new_Addr_def)
     2.1 --- a/src/HOL/Bali/Type.thy	Fri May 21 21:14:18 2004 +0200
     2.2 +++ b/src/HOL/Bali/Type.thy	Fri May 21 21:14:52 2004 +0200
     2.3 @@ -51,7 +51,7 @@
     2.4  
     2.5  constdefs
     2.6    the_Class :: "ty \<Rightarrow> qtname"
     2.7 - "the_Class T \<equiv> \<epsilon> C. T = Class C" (** primrec not possible here **)
     2.8 + "the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **)
     2.9   
    2.10  lemma the_Class_eq [simp]: "the_Class (Class C)= C"
    2.11  by (auto simp add: the_Class_def)
     3.1 --- a/src/HOL/Infinite_Set.thy	Fri May 21 21:14:18 2004 +0200
     3.2 +++ b/src/HOL/Infinite_Set.thy	Fri May 21 21:14:52 2004 +0200
     3.3 @@ -245,8 +245,8 @@
     3.4    assumes inf: "infinite (S::'a set)"
     3.5    shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
     3.6  proof -
     3.7 -  def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {\<epsilon> e. e \<in> T})"
     3.8 -  def pick \<equiv> "\<lambda>n. (\<epsilon> e. e \<in> Sseq n)"
     3.9 +  def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
    3.10 +  def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
    3.11    have Sseq_inf: "\<And>n. infinite (Sseq n)"
    3.12    proof -
    3.13      fix n