equal
deleted
inserted
replaced
9 |
9 |
10 theory BNF_Def |
10 theory BNF_Def |
11 imports BNF_Util |
11 imports BNF_Util |
12 keywords |
12 keywords |
13 "print_bnfs" :: diag and |
13 "print_bnfs" :: diag and |
14 "bnf_def" :: thy_goal |
14 "bnf" :: thy_goal |
15 begin |
15 begin |
16 |
16 |
17 lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)" |
17 lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)" |
18 by (rule ext) (auto simp only: o_apply collect_def) |
18 by (rule ext) (auto simp only: o_apply collect_def) |
19 |
19 |