equal
deleted
inserted
replaced
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" |
287 lemma Let_const: "Let x (\<lambda>_. c) = c" |
288 unfolding Let_def .. |
288 unfolding Let_def .. |
289 |
289 |
290 ML_file "Tools/BNF/bnf_fp_util_tactics.ML" |
290 ML_file \<open>Tools/BNF/bnf_fp_util_tactics.ML\<close> |
291 ML_file "Tools/BNF/bnf_fp_util.ML" |
291 ML_file \<open>Tools/BNF/bnf_fp_util.ML\<close> |
292 ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML" |
292 ML_file \<open>Tools/BNF/bnf_fp_def_sugar_tactics.ML\<close> |
293 ML_file "Tools/BNF/bnf_fp_def_sugar.ML" |
293 ML_file \<open>Tools/BNF/bnf_fp_def_sugar.ML\<close> |
294 ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML" |
294 ML_file \<open>Tools/BNF/bnf_fp_n2m_tactics.ML\<close> |
295 ML_file "Tools/BNF/bnf_fp_n2m.ML" |
295 ML_file \<open>Tools/BNF/bnf_fp_n2m.ML\<close> |
296 ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML" |
296 ML_file \<open>Tools/BNF/bnf_fp_n2m_sugar.ML\<close> |
297 |
297 |
298 end |
298 end |