equal
deleted
inserted
replaced
282 |
282 |
283 lemma convol_transfer: |
283 lemma convol_transfer: |
284 "rel_fun (rel_fun R S) (rel_fun (rel_fun R T) (rel_fun R (rel_prod S T))) BNF_Def.convol BNF_Def.convol" |
284 "rel_fun (rel_fun R S) (rel_fun (rel_fun R T) (rel_fun R (rel_prod S T))) BNF_Def.convol BNF_Def.convol" |
285 unfolding rel_fun_def convol_def by auto |
285 unfolding rel_fun_def convol_def by auto |
286 |
286 |
|
287 lemma Let_const: "Let x (\<lambda>_. c) = c" |
|
288 unfolding Let_def .. |
|
289 |
287 ML_file "Tools/BNF/bnf_fp_util_tactics.ML" |
290 ML_file "Tools/BNF/bnf_fp_util_tactics.ML" |
288 ML_file "Tools/BNF/bnf_fp_util.ML" |
291 ML_file "Tools/BNF/bnf_fp_util.ML" |
289 ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML" |
292 ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML" |
290 ML_file "Tools/BNF/bnf_fp_def_sugar.ML" |
293 ML_file "Tools/BNF/bnf_fp_def_sugar.ML" |
291 ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML" |
294 ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML" |