equal
deleted
inserted
replaced
204 proof  
204 proof  
205 case antecedent from this TrueI 
205 case antecedent from this TrueI 
206 show ?thesis by (rule quot_cond_function) 
206 show ?thesis by (rule quot_cond_function) 
207 qed 
207 qed 
208 
208 

209 theorem quot_function': 

210 "(!!X Y. f X Y == g (pick X) (pick Y)) ==> 

211 (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==> 

212 f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" 

213 by (rule quot_function) (simp only: quot_equality)+ 

214 
209 end 
215 end 