equal
deleted
inserted
replaced
29 thm even_odd.intros |
29 thm even_odd.intros |
30 |
30 |
31 simple_inductive |
31 simple_inductive |
32 accpart for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
32 accpart for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
33 where |
33 where |
34 accpartI: "(\<forall>y. r y x \<longrightarrow> accpart r y) \<Longrightarrow> accpart r x" |
34 accpartI: "(\<And>y. r y x \<Longrightarrow> accpart r y) \<Longrightarrow> accpart r x" |
35 |
35 |
36 thm accpart_def |
36 thm accpart_def |
37 thm accpart.induct |
37 thm accpart.induct |
38 thm accpartI |
38 thm accpartI |
39 |
39 |
51 thm accpart'.induct |
51 thm accpart'.induct |
52 end |
52 end |
53 |
53 |
54 thm rel.accpartI' |
54 thm rel.accpartI' |
55 thm rel.accpart'.induct |
55 thm rel.accpart'.induct |
56 |
|
57 |
|
58 lemma "True" by simp |
|
59 *) |
56 *) |
60 |
57 |
61 use_chunks "simple_inductive_package.ML" |
58 use_chunks "simple_inductive_package.ML" |
62 |
59 |
63 |
60 |