| changeset 284 | a21fb87bb0bd |
| parent 271 | 4457185b22ef |
| 283:7d29c3c09bea | 284:a21fb87bb0bd |
|---|---|
657 |
657 |
658 lemma uf_lemma [simp]: |
658 lemma uf_lemma [simp]: |
659 "rec_eval rec_uf [m, cf] = UF m cf" |
659 "rec_eval rec_uf [m, cf] = UF m cf" |
660 by (simp add: rec_uf_def) |
660 by (simp add: rec_uf_def) |
661 |
661 |
662 value "size rec_uf" |
662 (* value "size rec_uf" *) |
663 end |
663 end |
664 |
664 |