equal
deleted
inserted
replaced
306 unfolding convol_def image2p_def by fastforce |
306 unfolding convol_def image2p_def by fastforce |
307 |
307 |
308 lemma fun_rel_image2p: "(fun_rel R (image2p f g R)) f g" |
308 lemma fun_rel_image2p: "(fun_rel R (image2p f g R)) f g" |
309 unfolding fun_rel_def image2p_def by auto |
309 unfolding fun_rel_def image2p_def by auto |
310 |
310 |
|
311 ML_file "Tools/bnf_gfp_rec_sugar_tactics.ML" |
|
312 ML_file "Tools/bnf_gfp_rec_sugar.ML" |
311 ML_file "Tools/bnf_gfp_util.ML" |
313 ML_file "Tools/bnf_gfp_util.ML" |
312 ML_file "Tools/bnf_gfp_tactics.ML" |
314 ML_file "Tools/bnf_gfp_tactics.ML" |
313 ML_file "Tools/bnf_gfp.ML" |
315 ML_file "Tools/bnf_gfp.ML" |
314 |
316 |
315 end |
317 end |