equal
deleted
inserted
replaced
138 thm tree.dist_eqs |
138 thm tree.dist_eqs |
139 thm tree.inverts |
139 thm tree.inverts |
140 thm tree.injects |
140 thm tree.injects |
141 |
141 |
142 text {* Rules about case combinator *} |
142 text {* Rules about case combinator *} |
143 term tree_when |
143 term tree_case |
144 thm tree.tree_when_def |
144 thm tree.tree_case_def |
145 thm tree.when_rews |
145 thm tree.case_rews |
146 |
146 |
147 text {* Rules about selectors *} |
147 text {* Rules about selectors *} |
148 term left |
148 term left |
149 term right |
149 term right |
150 thm tree.sel_rews |
150 thm tree.sel_rews |