equal
deleted
inserted
replaced
95 code_pred |
95 code_pred |
96 (modes: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool) |
96 (modes: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool) |
97 [inductify] |
97 [inductify] |
98 subcls' |
98 subcls' |
99 . |
99 . |
100 lemma subcls_conv_subcls' [code_inline]: |
100 lemma subcls_conv_subcls' [code_unfold]: |
101 "(subcls1 G)^* = (\<lambda>(C, D). subcls' G C D)" |
101 "(subcls1 G)^* = (\<lambda>(C, D). subcls' G C D)" |
102 by(simp add: subcls'_def subcls1_def rtrancl_def)(simp add: Collect_def) |
102 by(simp add: subcls'_def subcls1_def rtrancl_def)(simp add: Collect_def) |
103 |
103 |
104 lemma class_rec_code [code]: |
104 lemma class_rec_code [code]: |
105 "class_rec G C t f = |
105 "class_rec G C t f = |