| changeset 244 | dc95a56b1953 |
| parent 189 | 069d525f8f1d |
| child 316 | 74f0a06f751f |
| 243:6e0f56764ff8 | 244:dc95a56b1953 |
|---|---|
42 |
42 |
43 simple_inductive (in rel) accpart' |
43 simple_inductive (in rel) accpart' |
44 where |
44 where |
45 accpartI': "\<And>x. (\<And>y. r y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x" |
45 accpartI': "\<And>x. (\<And>y. r y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x" |
46 |
46 |
47 |
|
48 context rel |
47 context rel |
49 begin |
48 begin |
50 thm accpartI' |
49 thm accpartI' |
51 thm accpart'.induct |
50 thm accpart'.induct |
52 end |
51 end |