src/HOL/Bali/WellType.thy
changeset 46212 d86ef6b96097
parent 41778 5f79a9e42507
child 46714 a7ca72710dfe
     1.1 --- a/src/HOL/Bali/WellType.thy	Sat Jan 14 16:12:09 2012 +0100
     1.2 +++ b/src/HOL/Bali/WellType.thy	Sat Jan 14 16:14:22 2012 +0100
     1.3 @@ -108,7 +108,7 @@
     1.4  
     1.5  definition
     1.6    --{* applicable methods, cf. 15.11.2.1 *}
     1.7 -  appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
     1.8 +  appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list) set" where
     1.9    "appl_methds G S rt = (\<lambda> sig. 
    1.10        {(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 
    1.11                             G\<turnstile>(parTs sig)[\<preceq>]pTs'})"
    1.12 @@ -121,7 +121,7 @@
    1.13  
    1.14  definition
    1.15    --{* maximally specific methods, cf. 15.11.2.2 *}
    1.16 -  max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
    1.17 +  max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list) set" where
    1.18    "max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and>
    1.19                            (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
    1.20