src/HOL/Bali/Table.thy
changeset 30235 58d147683393
parent 24194 96013f81faef
child 34939 44294cfecb1d
     1.1 --- a/src/HOL/Bali/Table.thy	Tue Mar 03 17:05:18 2009 +0100
     1.2 +++ b/src/HOL/Bali/Table.thy	Wed Mar 04 10:47:20 2009 +0100
     1.3 @@ -194,7 +194,7 @@
     1.4  done
     1.5  
     1.6  lemma Ball_set_tableD: 
     1.7 -  "\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> o2s (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"
     1.8 +  "\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> Option.set (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"
     1.9  apply (frule Ball_set_table)
    1.10  by auto
    1.11