equal
deleted
inserted
replaced
174 term tree_finite |
174 term tree_finite |
175 thm tree.finite_def |
175 thm tree.finite_def |
176 thm tree.finites |
176 thm tree.finites |
177 |
177 |
178 text {* Rules about bisimulation predicate *} |
178 text {* Rules about bisimulation predicate *} |
179 (* COINDUCTION TEMPORARILY DISABLED |
|
180 term tree_bisim |
179 term tree_bisim |
181 thm tree.bisim_def |
180 thm tree.bisim_def |
182 thm tree.coind |
181 thm tree.coind |
183 COINDUCTION TEMPORARILY DISABLED *) |
|
184 |
182 |
185 text {* Induction rule *} |
183 text {* Induction rule *} |
186 thm tree.ind |
184 thm tree.ind |
187 |
185 |
188 |
186 |