equal
deleted
inserted
replaced
10 |
10 |
11 theory BNF_Def |
11 theory BNF_Def |
12 imports BNF_Cardinal_Arithmetic Fun_Def_Base |
12 imports BNF_Cardinal_Arithmetic Fun_Def_Base |
13 keywords |
13 keywords |
14 "print_bnfs" :: diag and |
14 "print_bnfs" :: diag and |
15 "bnf" :: thy_goal |
15 "bnf" :: thy_goal_defn |
16 begin |
16 begin |
17 |
17 |
18 lemma Collect_case_prodD: "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)" |
18 lemma Collect_case_prodD: "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)" |
19 by auto |
19 by auto |
20 |
20 |