| changeset 346 | 0fea8b7a14a1 |
| parent 295 | 24c68350d059 |
| child 359 | be6538c7b41d |
| 345:4c54ef4dc84d | 346:0fea8b7a14a1 |
|---|---|
1 theory Ind_General_Scheme |
1 theory Ind_General_Scheme |
2 imports "../Base" Simple_Inductive_Package |
2 imports Ind_Intro Simple_Inductive_Package |
3 begin |
3 begin |
4 |
4 |
5 (*<*) |
5 (*<*) |
6 simple_inductive |
6 simple_inductive |
7 trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
7 trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |