| changeset 760 | f0200e91b272 |
| parent 576 | 469279790410 |
| child 782 | 200a16083201 |
--- a/src/ZF/ex/LList.ML Wed Dec 07 12:34:47 1994 +0100 +++ b/src/ZF/ex/LList.ML Wed Dec 07 13:12:04 1994 +0100 @@ -184,7 +184,7 @@ by (asm_simp_tac flip_ss 1); by (asm_simp_tac flip_ss 1); by (fast_tac (ZF_cs addSIs [not_type]) 1); -val flip_type = result(); +qed "flip_type"; val [prem] = goal LList.thy "l : llist(bool) ==> flip(flip(l)) = l";