equal
deleted
inserted
replaced
319 by auto |
319 by auto |
320 |
320 |
321 lemma list_rec_Cons: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)" |
321 lemma list_rec_Cons: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)" |
322 by auto |
322 by auto |
323 |
323 |
324 lemma sum_case_cong: "p = q \<Longrightarrow> sum_case f g p = sum_case f g q" |
|
325 by simp |
|
326 |
|
327 lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y" |
324 lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y" |
328 by simp |
325 by simp |
329 |
326 |
330 ML_file "Tools/bnf_gfp_util.ML" |
327 ML_file "Tools/bnf_gfp_util.ML" |
331 ML_file "Tools/bnf_gfp_tactics.ML" |
328 ML_file "Tools/bnf_gfp_tactics.ML" |