equal
deleted
inserted
replaced
263 unfolding eq_onp_def by simp |
263 unfolding eq_onp_def by simp |
264 |
264 |
265 lemma Ball_image_comp: "Ball (f ` A) g = Ball A (g o f)" |
265 lemma Ball_image_comp: "Ball (f ` A) g = Ball A (g o f)" |
266 by auto |
266 by auto |
267 |
267 |
|
268 lemma rel_fun_Collect_case_prodD: |
|
269 "rel_fun A B f g \<Longrightarrow> X \<subseteq> Collect (case_prod A) \<Longrightarrow> x \<in> X \<Longrightarrow> B ((f o fst) x) ((g o snd) x)" |
|
270 unfolding rel_fun_def by auto |
|
271 |
268 ML_file "Tools/BNF/bnf_util.ML" |
272 ML_file "Tools/BNF/bnf_util.ML" |
269 ML_file "Tools/BNF/bnf_tactics.ML" |
273 ML_file "Tools/BNF/bnf_tactics.ML" |
270 ML_file "Tools/BNF/bnf_def_tactics.ML" |
274 ML_file "Tools/BNF/bnf_def_tactics.ML" |
271 ML_file "Tools/BNF/bnf_def.ML" |
275 ML_file "Tools/BNF/bnf_def.ML" |
272 |
276 |